let C be concrete category; :: thesis: 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; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for f being Morphism of a,b st f is iso holds
f " = f " )
assume A1: ( <^a,b^> <> {} & <^b,a^> <> {} ) ; :: thesis: for f being Morphism of a,b st f is iso holds
f " = f "
let f be Morphism of a,b; :: thesis: ( f is iso implies f " = f " )
assume A2: f is iso ; :: thesis: f " = f "
then A3: (f " ) * f = idm a by ALTCAT_3:def 5;
A4: (f " ) * f = (f " ) * f by A1, Th38;
A5: ( dom (f " ) = the_carrier_of b & dom f = the_carrier_of a ) by A1, Th36;
A6: ( f is one-to-one & rng f = the_carrier_of b ) by A1, A2, Th42;
idm a = id (the_carrier_of a) by Def10;
hence f " = f " by A3, A4, A5, A6, FUNCT_1:63; :: thesis: verum