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 object holds
( y in dom (" (g * f)) iff y in dom ((" f) * (" g)) )

proof

let y be object ; :: thesis: ( y in dom (" (g * f)) iff y in dom ((" f) * (" g)) )
reconsider yy = y as set by TARSKI:1;
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: yy c= rng g by A2;
then y in bool (rng g) ;
then A4: y in dom (" g) by Def2;
g " yy c= rng f by A1, A2, Th4;
then g " yy in bool (rng f) ;
then g " yy 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 " yy in dom (" f) by A6, Th21;
then A7: g " yy in bool (rng f) by Def2;
y in bool (rng g) by A6, Def2;
then yy 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:2;
for y being object st y in dom (" (g * f)) holds
(" (g * f)) . y = ((" f) * (" g)) . y

proof

let y be object ; :: 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;
reconsider yy = y as set by TARSKI:1;
A11: g " yy c= rng f by A1, Th4, A10;
rng (g * f) c= rng g by RELAT_1:26;
then A12: yy c= rng g by A10;
then y in bool (rng g) ;
then A13: y in dom (" g) by Def2;
thus (" (g * f)) . y = (g * f) " yy by A9, Th21
.= f " (g " yy) by RELAT_1:146
.= (" f) . (g " yy) 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; :: thesis: verum