let C be semi-functional para-functional category; :: thesis: 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; :: thesis: ( <^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^> <> {} ; :: thesis: 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; :: thesis: ( f is one-to-one & f " in <^b,a^> implies f is iso )
assume A2: f is one-to-one ; :: thesis: ( not f " in <^b,a^> or f is iso )
assume A3: f " in <^b,a^> ; :: thesis: 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) & f * (f " ) = id (rng f) ) by A2, FUNCT_1:61;
dom f = the_carrier_of a by A1, Th36;
then ( f * g = id (the_carrier_of b) & g * f = id (the_carrier_of a) ) by A1, A3, A4, A5, Th38;
then A6: ( idm b = f * g & idm a = g * f ) by Th39;
then A7: ( g is_left_inverse_of f & g is_right_inverse_of f ) by ALTCAT_3:def 1;
then ( f is retraction & f is coretraction ) by ALTCAT_3:def 2, ALTCAT_3:def 3;
hence ( f * (f " ) = idm b & (f " ) * f = idm a ) by A1, A3, A6, A7, ALTCAT_3:def 4; :: according to ALTCAT_3:def 5 :: thesis: verum