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, Th36;
then A4:
rng f = the_carrier_of b
by A2, FUNCT_1:55;
A5:
(f " ) * f = id (dom f)
by A2, FUNCT_1:61;
A6:
f * (f " ) = id (rng f)
by A2, FUNCT_1:61;
A7:
dom f = the_carrier_of a
by A1, Th36;
A8:
f * g = id (the_carrier_of b)
by A1, A3, A4, A6, Th38;
A9:
g * f = id (the_carrier_of a)
by A1, A3, A5, A7, Th38;
A10:
idm b = f * g
by A8, Th39;
A11:
idm a = g * f
by A9, Th39;
then A12:
g is_left_inverse_of f
by ALTCAT_3:def 1;
A13:
g is_right_inverse_of f
by A10, ALTCAT_3:def 1;
then
( f is retraction & f is coretraction )
by A12, ALTCAT_3:def 2, ALTCAT_3:def 3;
hence
( f * (f " ) = idm b & (f " ) * f = idm a )
by A1, A3, A10, A11, A12, A13, ALTCAT_3:def 4; ALTCAT_3:def 5 verum