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: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; ALTCAT_3:def 5 verum