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

proof

let y be object ; :: 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 object such that
A3: x in dom (g * f) and
A4: y = (g * f) . x by Def3;
A5: f . x in dom g by A3, Th11;
A6: y = g . (f . x) by A3, A4, Th12;
then y in rng g by A5, Def3;
then A7: y in dom (g ") by A2, Th31;
A8: x in dom f by A3, Th11;
(g ") . (g . (f . x)) = ((g ") * g) . (f . x) by A5, Th13
.= (id (dom g)) . (f . x) by A2, Th38
.= f . x by A5, Th17 ;
then (g ") . y in rng f by A8, A6, Def3;
then (g ") . y in dom (f ") by A1, Th31;
hence y in dom ((f ") * (g ")) by A7, Th11; :: thesis: verum

end;

assume A9: y in dom ((f ") * (g ")) ; :: thesis: y in rng (g * f)
then y in dom (g ") by Th11;
then y in rng g by A2, Th31;
then consider z being object such that
A10: z in dom g and
A11: y = g . z by Def3;
(g ") . y in dom (f ") by A9, Th11;
then (g ") . (g . z) in rng f by A1, A11, Th31;
then ((g ") * g) . z in rng f by A10, Th13;
then (id (dom g)) . z in rng f by A2, Th38;
then z in rng f by A10, Th17;
then consider x being object such that
A12: ( x in dom f & z = f . x ) by Def3;
( x in dom (g * f) & y = (g * f) . x ) by A10, A11, A12, Th11, Th13;
hence y in rng (g * f) by Def3; :: thesis: verum

end;

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

proof

let x be object ; :: 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 Th11; :: 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 Def3;
hence x in dom (((f ") * (g ")) * (g * f)) by A13, A14, Th11; :: thesis: verum

end;

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

proof

let x be object ; :: 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 Th11;
(g * f) . x in rng (g * f) by A16, Def3;
then A18: g . (f . x) in dom ((f ") * (g ")) by A13, A16, Th12;
A19: x in dom f by A16, Th11;
thus (((f ") * (g ")) * (g * f)) . x = ((f ") * (g ")) . ((g * f) . x) by A15, A16, Th12
.= ((f ") * (g ")) . (g . (f . x)) by A16, Th12
.= (f ") . ((g ") . (g . (f . x))) by A18, Th12
.= (f ") . (((g ") * g) . (f . x)) by A17, Th13
.= (f ") . ((id (dom g)) . (f . x)) by A2, Th38
.= (f ") . (f . x) by A17, Th17
.= x by A1, A19, Th33 ; :: thesis: verum

end;

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