theorem Th5: :: WAYBEL27:5

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