let C be semi-functional para-functional category; for a, b being Object of C st <^a,b^> <> {} holds
for f being Morphism of a,b st f is one-to-one & f " in <^b,a^> holds
f is iso
let a, b be Object of C; ( <^a,b^> <> {} implies for f being Morphism of a,b st f is one-to-one & f " in <^b,a^> holds
f is iso )
assume A1:
<^a,b^> <> {}
; for f being Morphism of a,b st f is one-to-one & f " in <^b,a^> holds
f is iso
let f be Morphism of a,b; ( f is one-to-one & f " in <^b,a^> implies f is iso )
assume A2:
f is one-to-one
; ( not f " in <^b,a^> or f is iso )
assume A3:
f " in <^b,a^>
; f is iso
then reconsider g = f " as Morphism of b,a ;
dom g = the_carrier_of b
by A3, Th35;
then A4:
rng f = the_carrier_of b
by A2, FUNCT_1:33;
A5:
(f ") * f = id (dom f)
by A2, FUNCT_1:39;
A6:
f * (f ") = id (rng f)
by A2, FUNCT_1:39;
A7:
dom f = the_carrier_of a
by A1, Th35;
A8:
f * g = id (the_carrier_of b)
by A1, A3, A4, A6, Th36;
A9:
g * f = id (the_carrier_of a)
by A1, A3, A5, A7, Th36;
A10:
idm b = f * g
by A8, Th37;
idm a = g * f
by A9, Th37;
then A11:
g is_left_inverse_of f
;
A12:
g is_right_inverse_of f
by A10;
then
( f is retraction & f is coretraction )
by A11;
hence
( f * (f ") = idm b & (f ") * f = idm a )
by A1, A3, A11, A12, ALTCAT_3:def 4; ALTCAT_3:def 5 verum