let C be category; :: thesis: 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; :: thesis: ( 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
; :: thesis: ( not <^o2,o1^> <> {} or ( o2 is initial & o1 is terminal ) )
assume
<^o2,o1^> <> {}
; :: thesis: ( o2 is initial & o1 is terminal )
then consider m being set such that
A3:
m in <^o2,o1^>
by XBOOLE_0:def 1;
reconsider m = m as Morphism of o2,o1 by A3;
consider l being Morphism of o1,o2 such that
A4:
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;
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;
:: thesis: 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^> & ( for
M1 being
Morphism of
o1,
o3 st
M1 in <^o1,o3^> holds
M = M1 ) )
by A1, ALTCAT_3:25;
take
M * m
;
:: thesis: ( M * m in <^o2,o3^> & ( for M1 being Morphism of o2,o3 st M1 in <^o2,o3^> holds
M * m = M1 ) )
<^o2,o3^> <> {}
by A3, A5, ALTCAT_1:def 4;
hence
M * m in <^o2,o3^>
;
:: thesis: for M1 being Morphism of o2,o3 st M1 in <^o2,o3^> holds
M * m = M1
let M1 be
Morphism of
o2,
o3;
:: thesis: ( M1 in <^o2,o3^> implies M * m = M1 )
assume A6:
M1 in <^o2,o3^>
;
:: thesis: M * m = M1
consider i2 being
Morphism of
o2,
o2 such that
i2 in <^o2,o2^>
and A7:
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
.=
M1 * (l * m)
by A3, A4, A6, ALTCAT_1:25
.=
M1 * i2
by A7
.=
M1 * (idm o2)
by A7
.=
M1
by A6, ALTCAT_1:def 19
;
:: thesis: verum
end;
hence
o2 is initial
by ALTCAT_3:25; :: thesis: 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;
:: thesis: 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 A8:
(
M in <^o3,o2^> & ( for
M1 being
Morphism of
o3,
o2 st
M1 in <^o3,o2^> holds
M = M1 ) )
by A2, ALTCAT_3:27;
take
m * M
;
:: thesis: ( m * M in <^o3,o1^> & ( for M1 being Morphism of o3,o1 st M1 in <^o3,o1^> holds
m * M = M1 ) )
<^o3,o1^> <> {}
by A3, A8, ALTCAT_1:def 4;
hence
m * M in <^o3,o1^>
;
:: thesis: for M1 being Morphism of o3,o1 st M1 in <^o3,o1^> holds
m * M = M1
let M1 be
Morphism of
o3,
o1;
:: thesis: ( M1 in <^o3,o1^> implies m * M = M1 )
assume A9:
M1 in <^o3,o1^>
;
:: thesis: m * M = M1
consider i1 being
Morphism of
o1,
o1 such that
i1 in <^o1,o1^>
and A10:
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 A8
.=
(m * l) * M1
by A3, A4, A9, ALTCAT_1:25
.=
i1 * M1
by A10
.=
(idm o1) * M1
by A10
.=
M1
by A9, ALTCAT_1:24
;
:: thesis: verum
end;
hence
o1 is terminal
by ALTCAT_3:27; :: thesis: verum