let C be lattice-wise with_all_isomorphisms category; :: thesis: for a, b being object of C
for f being Morphism of a,b st @ f is isomorphic holds
f is iso
let a, b be object of C; :: thesis: for f being Morphism of a,b st @ f is isomorphic holds
f is iso
let f be Morphism of a,b; :: thesis: ( @ f is isomorphic implies f is iso )
assume A1: @ f is isomorphic ; :: thesis: f is iso
then consider g being monotone Function of (latt b),(latt a) such that
A2: ( (@ f) * g = id (latt b) & g * (@ f) = id (latt a) ) by YELLOW16:17;
A3: ( idm a = id (latt a) & idm b = id (latt b) ) by Th2;
A4: g is isomorphic by A2, YELLOW16:17;
then A5: ( @ f in <^a,b^> & g in <^b,a^> ) by A1, Def8;
reconsider g = g as Morphism of b,a by A4, Def8;
@ g = g by A5, Def7;
then A6: ( f * g = idm b & g * f = idm a ) by A2, A3, A5, Th3;
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 A5, A6, A7, ALTCAT_3:def 4; :: according to ALTCAT_3:def 5 :: thesis: verum