let C be category; :: thesis: 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; :: thesis: ( o2 is terminal & o1,o2 are_iso implies o1 is terminal )

assume that

A1: o2 is terminal and

A2: o1,o2 are_iso ; :: thesis: 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 ) )

o1 is terminal

let o1, o2 be Object of C; :: thesis: ( o2 is terminal & o1,o2 are_iso implies o1 is terminal )

assume that

A1: o2 is terminal and

A2: o1,o2 are_iso ; :: thesis: 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

hence
o1 is terminal
by ALTCAT_3:27; :: thesis: verum
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; :: thesis: 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 ; :: thesis: ( (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^> ; :: thesis: 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; :: thesis: ( v in <^o3,o1^> implies (f ") * u = v )

assume v in <^o3,o1^> ; :: thesis: (f ") * u = v

f * v = u by A5, A6;

hence (f ") * u = v by A4, A9, A7, A8, Th1; :: thesis: verum

end;A3: f is iso by A2;

A4: (f ") * f = idm o1 by A3;

let o3 be Object of C; :: thesis: 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 ; :: thesis: ( (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^> ; :: thesis: 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; :: thesis: ( v in <^o3,o1^> implies (f ") * u = v )

assume v in <^o3,o1^> ; :: thesis: (f ") * u = v

f * v = u by A5, A6;

hence (f ") * u = v by A4, A9, A7, A8, Th1; :: thesis: verum