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 ) )

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^> <> {} ; :: thesis: ( 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 ) )

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 ) )

( 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 ) )

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^> <> {} ; :: thesis: ( 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

hence
o2 is initial
by ALTCAT_3:25; :: thesis: o1 is terminal
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^> 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 ; :: 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 A4, A5, ALTCAT_1:def 2;

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 A7: M1 in <^o2,o3^> ; :: thesis: 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 ; :: thesis: verum

end;( 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 ; :: 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 A4, A5, ALTCAT_1:def 2;

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 A7: M1 in <^o2,o3^> ; :: thesis: 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 ; :: thesis: verum

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

hence
o1 is terminal
by ALTCAT_3:27; :: thesis: verum
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

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 ; :: 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 A4, A9, ALTCAT_1:def 2;

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 A11: M1 in <^o3,o1^> ; :: thesis: 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 ; :: thesis: verum

end;( 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 ; :: 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 A4, A9, ALTCAT_1:def 2;

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 A11: M1 in <^o3,o1^> ; :: thesis: 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 ; :: thesis: verum