let C be category; for o1, o2 being Object of C st o1 is initial & o2 is terminal & <^o2,o1^> <> {} holds
( o2 is initial & o1 is terminal )
let o1, o2 be Object of C; ( o1 is initial & o2 is terminal & <^o2,o1^> <> {} implies ( o2 is initial & o1 is terminal ) )
assume that
A1:
o1 is initial
and
A2:
o2 is terminal
; ( not <^o2,o1^> <> {} or ( o2 is initial & o1 is terminal ) )
consider l being Morphism of o1,o2 such that
A3:
l in <^o1,o2^>
and
for M1 being Morphism of o1,o2 st M1 in <^o1,o2^> holds
l = M1
by A1, ALTCAT_3:25;
assume
<^o2,o1^> <> {}
; ( o2 is initial & o1 is terminal )
then consider m being object such that
A4:
m in <^o2,o1^>
by XBOOLE_0:def 1;
reconsider m = m as Morphism of o2,o1 by A4;
for o3 being Object of C ex M being Morphism of o2,o3 st
( M in <^o2,o3^> & ( for M1 being Morphism of o2,o3 st M1 in <^o2,o3^> holds
M = M1 ) )
proof
let o3 be
Object of
C;
ex M being Morphism of o2,o3 st
( M in <^o2,o3^> & ( for M1 being Morphism of o2,o3 st M1 in <^o2,o3^> holds
M = M1 ) )
consider M being
Morphism of
o1,
o3 such that A5:
M in <^o1,o3^>
and A6:
for
M1 being
Morphism of
o1,
o3 st
M1 in <^o1,o3^> holds
M = M1
by A1, ALTCAT_3:25;
take
M * m
;
( M * m in <^o2,o3^> & ( for M1 being Morphism of o2,o3 st M1 in <^o2,o3^> holds
M * m = M1 ) )
<^o2,o3^> <> {}
by A4, A5, ALTCAT_1:def 2;
hence
M * m in <^o2,o3^>
;
for M1 being Morphism of o2,o3 st M1 in <^o2,o3^> holds
M * m = M1
let M1 be
Morphism of
o2,
o3;
( M1 in <^o2,o3^> implies M * m = M1 )
assume A7:
M1 in <^o2,o3^>
;
M * m = M1
consider i2 being
Morphism of
o2,
o2 such that
i2 in <^o2,o2^>
and A8:
for
M1 being
Morphism of
o2,
o2 st
M1 in <^o2,o2^> holds
i2 = M1
by A2, ALTCAT_3:27;
thus M * m =
(M1 * l) * m
by A5, A6
.=
M1 * (l * m)
by A4, A3, A7, ALTCAT_1:21
.=
M1 * i2
by A8
.=
M1 * (idm o2)
by A8
.=
M1
by A7, ALTCAT_1:def 17
;
verum
end;
hence
o2 is initial
by ALTCAT_3:25; o1 is terminal
for o3 being Object of C ex M being Morphism of o3,o1 st
( M in <^o3,o1^> & ( for M1 being Morphism of o3,o1 st M1 in <^o3,o1^> holds
M = M1 ) )
proof
let o3 be
Object of
C;
ex M being Morphism of o3,o1 st
( M in <^o3,o1^> & ( for M1 being Morphism of o3,o1 st M1 in <^o3,o1^> holds
M = M1 ) )
consider M being
Morphism of
o3,
o2 such that A9:
M in <^o3,o2^>
and A10:
for
M1 being
Morphism of
o3,
o2 st
M1 in <^o3,o2^> holds
M = M1
by A2, ALTCAT_3:27;
take
m * M
;
( m * M in <^o3,o1^> & ( for M1 being Morphism of o3,o1 st M1 in <^o3,o1^> holds
m * M = M1 ) )
<^o3,o1^> <> {}
by A4, A9, ALTCAT_1:def 2;
hence
m * M in <^o3,o1^>
;
for M1 being Morphism of o3,o1 st M1 in <^o3,o1^> holds
m * M = M1
let M1 be
Morphism of
o3,
o1;
( M1 in <^o3,o1^> implies m * M = M1 )
assume A11:
M1 in <^o3,o1^>
;
m * M = M1
consider i1 being
Morphism of
o1,
o1 such that
i1 in <^o1,o1^>
and A12:
for
M1 being
Morphism of
o1,
o1 st
M1 in <^o1,o1^> holds
i1 = M1
by A1, ALTCAT_3:25;
thus m * M =
m * (l * M1)
by A9, A10
.=
(m * l) * M1
by A4, A3, A11, ALTCAT_1:21
.=
i1 * M1
by A12
.=
(idm o1) * M1
by A12
.=
M1
by A11, ALTCAT_1:20
;
verum
end;
hence
o1 is terminal
by ALTCAT_3:27; verum