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

proof

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

proof

assume y in rng (g * f) ; :: thesis: y in dom ((f " ) * (g " ))
then consider x being set such that
A3: x in dom (g * f) and
A4: y = (g * f) . x by Def5;
A5: f . x in dom g by A3, Th21;
A6: y = g . (f . x) by A3, A4, Th22;
then y in rng g by A5, Def5;
then A7: y in dom (g " ) by A2, Th54;
A8: x in dom f by A3, Th21;
(g " ) . (g . (f . x)) = ((g " ) * g) . (f . x) by A5, Th23
.= (id (dom g)) . (f . x) by A2, Th61
.= f . x by A5, Th34 ;
then (g " ) . y in rng f by A8, A6, Def5;
then (g " ) . y in dom (f " ) by A1, Th54;
hence y in dom ((f " ) * (g " )) by A7, Th21; :: thesis: verum

end;

assume A9: y in dom ((f " ) * (g " )) ; :: thesis: y in rng (g * f)
then y in dom (g " ) by Th21;
then y in rng g by A2, Th54;
then consider z being set such that
A10: z in dom g and
A11: y = g . z by Def5;
(g " ) . y in dom (f " ) by A9, Th21;
then (g " ) . (g . z) in rng f by A1, A11, Th54;
then ((g " ) * g) . z in rng f by A10, Th23;
then (id (dom g)) . z in rng f by A2, Th61;
then z in rng f by A10, Th34;
then consider x being set such that
A12: ( x in dom f & z = f . x ) by Def5;
( x in dom (g * f) & y = (g * f) . x ) by A10, A11, A12, Th21, Th23;
hence y in rng (g * f) by Def5; :: thesis: verum

end;

then A13: rng (g * f) = dom ((f " ) * (g " )) by TARSKI:2;
for x being set holds
( x in dom (((f " ) * (g " )) * (g * f)) iff x in dom (g * f) )

proof

let x be set ; :: thesis: ( x in dom (((f " ) * (g " )) * (g * f)) iff x in dom (g * f) )
thus ( x in dom (((f " ) * (g " )) * (g * f)) implies x in dom (g * f) ) by Th21; :: thesis: ( x in dom (g * f) implies x in dom (((f " ) * (g " )) * (g * f)) )
assume A14: x in dom (g * f) ; :: thesis: x in dom (((f " ) * (g " )) * (g * f))
then (g * f) . x in rng (g * f) by Def5;
hence x in dom (((f " ) * (g " )) * (g * f)) by A13, A14, Th21; :: thesis: verum

end;

then A15: dom (((f " ) * (g " )) * (g * f)) = dom (g * f) by TARSKI:2;
for x being set st x in dom (g * f) holds
(((f " ) * (g " )) * (g * f)) . x = x

proof

let x be set ; :: thesis: ( x in dom (g * f) implies (((f " ) * (g " )) * (g * f)) . x = x )
assume A16: x in dom (g * f) ; :: thesis: (((f " ) * (g " )) * (g * f)) . x = x
then A17: f . x in dom g by Th21;
(g * f) . x in rng (g * f) by A16, Def5;
then A18: g . (f . x) in dom ((f " ) * (g " )) by A13, A16, Th22;
A19: x in dom f by A16, Th21;
thus (((f " ) * (g " )) * (g * f)) . x = ((f " ) * (g " )) . ((g * f) . x) by A15, A16, Th22
.= ((f " ) * (g " )) . (g . (f . x)) by A16, Th22
.= (f " ) . ((g " ) . (g . (f . x))) by A18, Th22
.= (f " ) . (((g " ) * g) . (f . x)) by A17, Th23
.= (f " ) . ((id (dom g)) . (f . x)) by A2, Th61
.= (f " ) . (f . x) by A17, Th34
.= x by A1, A19, Th56 ; :: thesis: verum

end;

then ((f " ) * (g " )) * (g * f) = id (dom (g * f)) by A15, Th34;
hence (g * f) " = (f " ) * (g " ) by A1, A2, A13, Th63; :: thesis: verum