Legyenek , , és tetszőleges típusok. Legyen továbbá és , valamint , és függvények.

Tekintsük az alábbi specifikációval adott feladatot:

Tegyük fel, hogy az függvény értékét kiszámító program az alábbi alakban írható fel:

Ha az , és programok végrehajtása nem változtatja meg az változó értékét, akkor a fenti programot elemenként előállító programnak nevezzük,

Hasonlóan, tegyük fel, hogy az függvény értékét kiszámító program pedig az alábbi formában írható fel:

Ha az , és programok végrehajtása nem változtatja meg az változó értékét, akkor a fenti programot elemenként felhasználó programnak nevezzük,

Tegyük fel továbbá, hogy az függvény elemenként feldolgozható, és minden egyelemű halmazra a függvényérték egyelemű. Ekkor a függvénykompozíció helyettesítési értékének kiszámítására vonatkozó programozási tétel alapján a feladat megoldható a fenti elemenként előállító, egy elemenként feldolgozó és az imént bemutatott elemenként felhasználó program szekvenciájaként.

A feladatra azonban egy hatékonyabb megoldást is adhatunk a programinverzió segítségével: ekkor a közbülső két sorozat típust kihagyhatjuk és a három ciklust egybeírhatjuk az alábbi módon: