let A, B, C be set ; :: thesis: 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)
let f be currying Function; :: thesis: for g being uncurrying Function st dom f c= Funcs [:A,B:],C & rng f c= dom g holds
g * f = id (dom f)
let g be uncurrying Function; :: thesis: ( dom f c= Funcs [:A,B:],C & rng f c= dom g implies g * f = id (dom f) )
assume A1: ( dom f c= Funcs [:A,B:],C & rng f c= dom g ) ; :: thesis: g * f = id (dom f)
then A2: dom (g * f) = dom f by RELAT_1:46;

now

let x be set ; :: thesis: ( x in dom f implies (g * f) . x = x )
assume A3: x in dom f ; :: thesis: (g * f) . x = x
then reconsider X = x as Function by Def2;
consider F being Function such that
A4: ( X = F & dom F = [:A,B:] & rng F c= C ) by A1, A3, FUNCT_2:def 2;
A5: f . x in rng f by A3, FUNCT_1:def 5;
then reconsider Y = f . x as Function by A1, Def1;
thus (g * f) . x = g . (f . x) by A3, FUNCT_1:23
.= uncurry Y by A1, A5, Def1
.= uncurry (curry X) by A3, Def2
.= x by A4, FUNCT_5:56 ; :: thesis: verum

end;

hence g * f = id (dom f) by A2, FUNCT_1:34; :: thesis: verum