let f be Function; :: thesis: ( f is one-to-one implies ( (f ") * f = id (dom f) & f * (f ") = id (rng f) ) )
assume A1: f is one-to-one ; :: thesis: ( (f ") * f = id (dom f) & f * (f ") = id (rng f) )
A2: for x being object st x in dom ((f ") * f) holds
((f ") * f) . x = x

proof

let x be object ; :: thesis: ( x in dom ((f ") * f) implies ((f ") * f) . x = x )
assume x in dom ((f ") * f) ; :: thesis: ((f ") * f) . x = x
then x in dom f by A1, Th35;
hence ((f ") * f) . x = x by A1, Th33; :: thesis: verum

end;

A3: for x being object st x in dom (f * (f ")) holds
(f * (f ")) . x = x

proof

let x be object ; :: thesis: ( x in dom (f * (f ")) implies (f * (f ")) . x = x )
assume x in dom (f * (f ")) ; :: thesis: (f * (f ")) . x = x
then x in rng f by A1, Th36;
hence (f * (f ")) . x = x by A1, Th34; :: thesis: verum

end;

dom ((f ") * f) = dom f by A1, Th35;
hence (f ") * f = id (dom f) by A2, Th17; :: thesis: f * (f ") = id (rng f)
dom (f * (f ")) = rng f by A1, Th36;
hence f * (f ") = id (rng f) by A3, Th17; :: thesis: verum