let f, g be Function; :: thesis: ( g is one-to-one implies " (g * f) = (" f) * (" g) )
assume A1: g is one-to-one ; :: thesis: " (g * f) = (" f) * (" g)
for y being set holds
( y in dom (" (g * f)) iff y in dom ((" f) * (" g)) )

proof

let y be set ; :: thesis: ( y in dom (" (g * f)) iff y in dom ((" f) * (" g)) )
thus ( y in dom (" (g * f)) implies y in dom ((" f) * (" g)) ) :: thesis: ( y in dom ((" f) * (" g)) implies y in dom (" (g * f)) )

proof

assume y in dom (" (g * f)) ; :: thesis: y in dom ((" f) * (" g))
then A2: y in bool (rng (g * f)) by Def2;
rng (g * f) c= rng g by RELAT_1:26;
then A3: y c= rng g by A2, XBOOLE_1:1;
then y in bool (rng g) ;
then A4: y in dom (" g) by Def2;
g " y c= rng f by A1, A2, Th4;
then g " y in bool (rng f) ;
then g " y in dom (" f) by Def2;
then (" g) . y in dom (" f) by A3, Def2;
hence y in dom ((" f) * (" g)) by A4, FUNCT_1:11; :: thesis: verum

end;

assume A5: y in dom ((" f) * (" g)) ; :: thesis: y in dom (" (g * f))
then A6: y in dom (" g) by FUNCT_1:11;
(" g) . y in dom (" f) by A5, FUNCT_1:11;
then g " y in dom (" f) by A6, Th24;
then A7: g " y in bool (rng f) by Def2;
y in bool (rng g) by A6, Def2;
then y c= rng (g * f) by A7, Th5;
then y in bool (rng (g * f)) ;
hence y in dom (" (g * f)) by Def2; :: thesis: verum

end;

then A8: dom (" (g * f)) = dom ((" f) * (" g)) by TARSKI:1;
for y being set st y in dom (" (g * f)) holds
(" (g * f)) . y = ((" f) * (" g)) . y

proof

let y be set ; :: thesis: ( y in dom (" (g * f)) implies (" (g * f)) . y = ((" f) * (" g)) . y )
assume A9: y in dom (" (g * f)) ; :: thesis: (" (g * f)) . y = ((" f) * (" g)) . y
then A10: y in bool (rng (g * f)) by Def2;
then A11: g " y c= rng f by A1, Th4;
rng (g * f) c= rng g by RELAT_1:26;
then A12: y c= rng g by A10, XBOOLE_1:1;
then y in bool (rng g) ;
then A13: y in dom (" g) by Def2;
thus (" (g * f)) . y = (g * f) " y by A9, Th24
.= f " (g " y) by RELAT_1:146
.= (" f) . (g " y) by A11, Def2
.= (" f) . ((" g) . y) by A12, Def2
.= ((" f) * (" g)) . y by A13, FUNCT_1:13 ; :: thesis: verum

end;

hence " (g * f) = (" f) * (" g) by A8, FUNCT_1:2; :: thesis: verum