theorem Th4: :: WAYBEL27:4

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