let C be category; for o1, o2 being Object of C st o2 is terminal & o1,o2 are_iso holds
o1 is terminal
let o1, o2 be Object of C; ( o2 is terminal & o1,o2 are_iso implies o1 is terminal )
assume that
A1:
o2 is terminal
and
A2:
o1,o2 are_iso
; o1 is terminal
for o3 being Object of C ex M being Morphism of o3,o1 st
( M in <^o3,o1^> & ( for v being Morphism of o3,o1 st v in <^o3,o1^> holds
M = v ) )
proof
consider f being
Morphism of
o1,
o2 such that A3:
f is
iso
by A2;
A4:
(f ") * f = idm o1
by A3;
let o3 be
Object of
C;
ex M being Morphism of o3,o1 st
( M in <^o3,o1^> & ( for v being Morphism of o3,o1 st v in <^o3,o1^> holds
M = v ) )
consider u being
Morphism of
o3,
o2 such that A5:
u in <^o3,o2^>
and A6:
for
M1 being
Morphism of
o3,
o2 st
M1 in <^o3,o2^> holds
u = M1
by A1, ALTCAT_3:27;
take
(f ") * u
;
( (f ") * u in <^o3,o1^> & ( for v being Morphism of o3,o1 st v in <^o3,o1^> holds
(f ") * u = v ) )
A7:
<^o2,o1^> <> {}
by A2;
then A8:
<^o3,o1^> <> {}
by A5, ALTCAT_1:def 2;
hence
(f ") * u in <^o3,o1^>
;
for v being Morphism of o3,o1 st v in <^o3,o1^> holds
(f ") * u = v
A9:
<^o1,o2^> <> {}
by A2;
let v be
Morphism of
o3,
o1;
( v in <^o3,o1^> implies (f ") * u = v )
assume
v in <^o3,o1^>
;
(f ") * u = v
f * v = u
by A5, A6;
hence
(f ") * u = v
by A4, A9, A7, A8, Th1;
verum
end;
hence
o1 is terminal
by ALTCAT_3:27; verum