theorem Th3: :: WAYBEL27:3

for A, B being non empty set
for C being set
for f, g being commuting Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds
g * f = id (dom f)