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