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