let A, B be non empty set ; :: thesis: 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)
let C be set ; :: thesis: 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)
let f, g be commuting 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

let x be set ; :: 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 Def3;
A5: f . x in rng f by A4, FUNCT_1:def 5;
then reconsider Y = f . x as Function by A2, Def3;
thus (g * f) . x = g . (f . x) by A4, FUNCT_1:23
.= commute Y by A2, A5, Def3
.= commute (commute X) by A4, Def3
.= x by A1, A4, FUNCT_6:87 ; :: thesis: verum

end;

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