let C be lattice-wise with_all_isomorphisms category; 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; for f being Morphism of a,b st @ f is isomorphic holds
f is iso
let f be Morphism of a,b; ( @ f is isomorphic implies f is iso )
assume A1:
@ f is isomorphic
; 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:17;
A4:
@ f in <^a,b^>
by A1, Def8;
A5:
g is isomorphic
by A2, A3, YELLOW16:17;
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 A8:
f * g = idm b
by A2, A4, A6, A7, Th3;
then A9:
g is_right_inverse_of f
by ALTCAT_3:def 1;
idm a = id (latt a)
by Th2;
then A10:
g * f = idm a
by A3, A4, A6, A7, Th3;
then A11:
g is_left_inverse_of f
by ALTCAT_3:def 1;
then
( f is retraction & f is coretraction )
by A9, ALTCAT_3:def 2, ALTCAT_3:def 3;
hence
( f * (f " ) = idm b & (f " ) * f = idm a )
by A4, A6, A8, A10, A11, A9, ALTCAT_3:def 4; ALTCAT_3:def 5 verum