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 y in bool (rng (g * f)) by Def2;
then ( y c= rng (g * f) & rng (g * f) c= rng g ) by RELAT_1:45;
then ( y c= rng g & g " y c= rng f ) by A1, Th4, XBOOLE_1:1;
then ( y in bool (rng g) & g " y in bool (rng f) ) ;
then ( y in dom (" g) & g " y in dom (" f) ) by Def2;
then ( y in dom (" g) & (" g) . y in dom (" f) ) by Th24;
hence y in dom ((" f) * (" g)) by FUNCT_1:21; :: thesis: verum

end;

assume y in dom ((" f) * (" g)) ; :: thesis: y in dom (" (g * f))
then ( y in dom (" g) & (" g) . y in dom (" f) ) by FUNCT_1:21;
then ( y in dom (" g) & g " y in dom (" f) ) by Th24;
then ( y in bool (rng g) & g " y in bool (rng f) ) by Def2;
then y c= rng (g * f) by Th5;
then y in bool (rng (g * f)) ;
hence y in dom (" (g * f)) by Def2; :: thesis: verum

end;

then A2: dom (" (g * f)) = dom ((" f) * (" g)) by TARSKI:2;
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 A3: y in dom (" (g * f)) ; :: thesis: (" (g * f)) . y = ((" f) * (" g)) . y
then y in bool (rng (g * f)) by Def2;
then ( y c= rng (g * f) & rng (g * f) c= rng g ) by RELAT_1:45;
then A4: ( y c= rng g & g " y c= rng f ) by A1, Th4, XBOOLE_1:1;
then ( y in bool (rng g) & g " y in bool (rng f) ) ;
then A5: ( y in dom (" g) & g " y in dom (" f) ) by Def2;
thus (" (g * f)) . y = (g * f) " y by A3, Th24
.= f " (g " y) by RELAT_1:181
.= (" f) . (g " y) by A4, Def2
.= (" f) . ((" g) . y) by A4, Def2
.= ((" f) * (" g)) . y by A5, FUNCT_1:23 ; :: thesis: verum

end;

hence " (g * f) = (" f) * (" g) by A2, FUNCT_1:9; :: thesis: verum