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
A4: x in dom (g * f) and
A5: y = (g * f) . x by Def5;
A6: ( x in dom f & f . x in dom g & y = g . (f . x) ) by A4, A5, Th21, Th22;
then y in rng g by Def5;
then A7: y in dom (g " ) by A2, Th54;
(g " ) . (g . (f . x)) = ((g " ) * g) . (f . x) by A6, Th23
.= (id (dom g)) . (f . x) by A2, Th61
.= f . x by A6, Th34 ;
then (g " ) . y in rng f by A6, Def5;
then (g " ) . y in dom (f " ) by A1, Th54;
hence y in dom ((f " ) * (g " )) by A7, Th21; :: thesis: verum

end;

assume y in dom ((f " ) * (g " )) ; :: thesis: y in rng (g * f)
then A8: ( y in dom (g " ) & (g " ) . y in dom (f " ) ) by Th21;
then y in rng g by A2, Th54;
then consider z being set such that
A9: z in dom g and
A10: y = g . z by Def5;
( (g " ) . (g . z) in rng f & g . z in dom (g " ) ) by A1, A8, A10, Th54;
then ((g " ) * g) . z in rng f by A9, Th23;
then (id (dom g)) . z in rng f by A2, Th61;
then z in rng f by A9, Th34;
then consider x being set such that
A11: x in dom f and
A12: z = f . x by Def5;
( x in dom (g * f) & y = (g * f) . x ) by A9, 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;
A18: x in dom f by A16, Th21;
(g * f) . x in rng (g * f) by A16, Def5;
then A19: g . (f . x) in dom ((f " ) * (g " )) by A13, A16, Th22;
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 A19, 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, A18, 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