let C be concrete category; for a, b being Object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is iso holds
f " = f "
let a, b be Object of C; ( <^a,b^> <> {} & <^b,a^> <> {} implies for f being Morphism of a,b st f is iso holds
f " = f " )
assume that
A1:
<^a,b^> <> {}
and
A2:
<^b,a^> <> {}
; for f being Morphism of a,b st f is iso holds
f " = f "
let f be Morphism of a,b; ( f is iso implies f " = f " )
assume A3:
f is iso
; f " = f "
then A4:
(f ") * f = idm a
;
A5:
(f ") * f = (f ") * f
by A1, A2, Th36;
A6:
dom (f ") = the_carrier_of b
by A2, Th35;
A7:
dom f = the_carrier_of a
by A1, Th35;
A8:
f is one-to-one
by A1, A2, A3, Th40;
A9:
rng f = the_carrier_of b
by A1, A2, A3, Th40;
idm a = id (the_carrier_of a)
by Def10;
hence
f " = f "
by A4, A5, A6, A7, A8, A9, FUNCT_1:41; verum