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) and
A3: g * (@ f) = id (latt a) by YELLOW16:15;
A4: @ f in <^a,b^> by A1, Def8;
A5: g is isomorphic by A2, A3, YELLOW16:15;
then A6: g in <^b,a^> by Def8;
reconsider g = g as Morphism of b,a by A5, Def8;
A7: @ g = g by A6, Def7;
idm b = id (latt b) by Th2;
then f * g = idm b by A2, A4, A6, A7, Th3;
then A8: g is_right_inverse_of f ;
idm a = id (latt a) by Th2;
then g * f = idm a by A3, A4, A6, A7, Th3;
then A9: g is_left_inverse_of f ;
then ( f is retraction & f is coretraction ) by A8;
hence ( f * (f ") = idm b & (f ") * f = idm a ) by A4, A6, A9, A8, ALTCAT_3:def 4; :: according to ALTCAT_3:def 5 :: thesis: verum