let C be category; :: thesis: 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; :: thesis: ( o1 is initial & o2 is initial implies o1,o2 are_iso )
assume that
A1: o1 is initial and
A2: o2 is initial ; :: thesis: o1,o2 are_iso
consider M1 being Morphism of o1,o2 such that
A3: ( M1 in <^o1,o2^> & <^o1,o2^> is trivial ) by A1, Def9;
consider M2 being Morphism of o2,o1 such that
A4: ( M2 in <^o2,o1^> & <^o2,o1^> is trivial ) by A2, Def9;
thus ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A3, A4; :: according to ALTCAT_3:def 6 :: thesis: ex A being Morphism of o1,o2 st A is iso
A5: ( ex M being Morphism of o1,o1 st
( M in <^o1,o1^> & <^o1,o1^> is trivial ) & ex N being Morphism of o2,o2 st
( N in <^o2,o2^> & <^o2,o2^> is trivial ) ) by A1, A2, Def9;
then consider x being set such that
A6: <^o1,o1^> = {x} by REALSET1:def 4;
consider y being set such that
A7: <^o2,o2^> = {y} by A5, REALSET1:def 4;
A8: ( M1 * M2 = y & M2 * M1 = x ) by A6, A7, TARSKI:def 1;
( idm o1 = x & idm o2 = y ) by A6, A7, TARSKI:def 1;
then ( M2 is_left_inverse_of M1 & M2 is_right_inverse_of M1 ) by A8, Def1;
then ( M1 is retraction & M1 is coretraction ) by Def2, Def3;
then M1 is iso by A3, A4, Th6;
hence ex A being Morphism of o1,o2 st A is iso ; :: thesis: verum