let C be category; for o1, o2 being Object of C st o1 is initial & o2 is initial holds
o1,o2 are_iso
let o1, o2 be Object of C; ( o1 is initial & o2 is initial implies o1,o2 are_iso )
assume that
A1:
o1 is initial
and
A2:
o2 is initial
; o1,o2 are_iso
ex N being Morphism of o2,o2 st
( N in <^o2,o2^> & <^o2,o2^> is trivial )
by A2;
then consider y being object such that
A3:
<^o2,o2^> = {y}
by ZFMISC_1:131;
consider M2 being Morphism of o2,o1 such that
A4:
M2 in <^o2,o1^>
and
<^o2,o1^> is trivial
by A2;
consider M1 being Morphism of o1,o2 such that
A5:
M1 in <^o1,o2^>
and
<^o1,o2^> is trivial
by A1;
thus
( <^o1,o2^> <> {} & <^o2,o1^> <> {} )
by A5, A4; ALTCAT_3:def 6 ex A being Morphism of o1,o2 st A is iso
( M1 * M2 = y & idm o2 = y )
by A3, TARSKI:def 1;
then
M2 is_right_inverse_of M1
;
then A6:
M1 is retraction
;
ex M being Morphism of o1,o1 st
( M in <^o1,o1^> & <^o1,o1^> is trivial )
by A1;
then consider x being object such that
A7:
<^o1,o1^> = {x}
by ZFMISC_1:131;
( M2 * M1 = x & idm o1 = x )
by A7, TARSKI:def 1;
then
M2 is_left_inverse_of M1
;
then
M1 is coretraction
;
then
M1 is iso
by A5, A4, A6, Th6;
hence
ex A being Morphism of o1,o2 st A is iso
; verum