let B be non empty set ; :: thesis: 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)
let A, C be set ; :: thesis: 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)
let f be uncurrying Function; :: thesis: 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)
let g be currying Function; :: thesis: ( dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g implies g * f = id (dom f) )
assume that
A1: dom f c= Funcs (A,(Funcs (B,C))) and
A2: rng f c= dom g ; :: thesis: g * f = id (dom f)

A3: now :: thesis: for x being object st x in dom f holds
(g * f) . x = x

let x be object ; :: thesis: ( x in dom f implies (g * f) . x = x )
assume A4: x in dom f ; :: thesis: (g * f) . x = x
then reconsider X = x as Function by Def1;
A5: ex F being Function st
( X = F & dom F = A & rng F c= Funcs (B,C) ) by A1, A4, FUNCT_2:def 2;
A6: f . x in rng f by A4, FUNCT_1:def 3;
then reconsider Y = f . x as Function by A2, Def2;
thus (g * f) . x = g . (f . x) by A4, FUNCT_1:13
.= curry Y by A2, A6, Def2
.= curry (uncurry X) by A4, Def1
.= x by A5, FUNCT_5:48 ; :: thesis: verum

end;

dom (g * f) = dom f by A2, RELAT_1:27;
hence g * f = id (dom f) by A3, FUNCT_1:17; :: thesis: verum