let C be category; :: thesis: for o1, o2 being Object of C st o1 is initial & o1,o2 are_iso holds

o2 is initial

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

assume that

A1: o1 is initial and

A2: o1,o2 are_iso ; :: thesis: o2 is initial

for o3 being Object of C ex M being Morphism of o2,o3 st

( M in <^o2,o3^> & ( for v being Morphism of o2,o3 st v in <^o2,o3^> holds

M = v ) )

o2 is initial

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

assume that

A1: o1 is initial and

A2: o1,o2 are_iso ; :: thesis: o2 is initial

for o3 being Object of C ex M being Morphism of o2,o3 st

( M in <^o2,o3^> & ( for v being Morphism of o2,o3 st v in <^o2,o3^> holds

M = v ) )

proof

hence
o2 is initial
by ALTCAT_3:25; :: thesis: verum
consider f being Morphism of o1,o2 such that

A3: f is iso by A2;

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

let o3 be Object of C; :: thesis: ex M being Morphism of o2,o3 st

( M in <^o2,o3^> & ( for v being Morphism of o2,o3 st v in <^o2,o3^> holds

M = v ) )

consider u being Morphism of o1,o3 such that

A5: u in <^o1,o3^> and

A6: for M1 being Morphism of o1,o3 st M1 in <^o1,o3^> holds

u = M1 by A1, ALTCAT_3:25;

take u * (f ") ; :: thesis: ( u * (f ") in <^o2,o3^> & ( for v being Morphism of o2,o3 st v in <^o2,o3^> holds

u * (f ") = v ) )

A7: <^o2,o1^> <> {} by A2;

then A8: <^o2,o3^> <> {} by A5, ALTCAT_1:def 2;

hence u * (f ") in <^o2,o3^> ; :: thesis: for v being Morphism of o2,o3 st v in <^o2,o3^> holds

u * (f ") = v

A9: <^o1,o2^> <> {} by A2;

let v be Morphism of o2,o3; :: thesis: ( v in <^o2,o3^> implies u * (f ") = v )

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

v * f = u by A5, A6;

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

end;A3: f is iso by A2;

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

let o3 be Object of C; :: thesis: ex M being Morphism of o2,o3 st

( M in <^o2,o3^> & ( for v being Morphism of o2,o3 st v in <^o2,o3^> holds

M = v ) )

consider u being Morphism of o1,o3 such that

A5: u in <^o1,o3^> and

A6: for M1 being Morphism of o1,o3 st M1 in <^o1,o3^> holds

u = M1 by A1, ALTCAT_3:25;

take u * (f ") ; :: thesis: ( u * (f ") in <^o2,o3^> & ( for v being Morphism of o2,o3 st v in <^o2,o3^> holds

u * (f ") = v ) )

A7: <^o2,o1^> <> {} by A2;

then A8: <^o2,o3^> <> {} by A5, ALTCAT_1:def 2;

hence u * (f ") in <^o2,o3^> ; :: thesis: for v being Morphism of o2,o3 st v in <^o2,o3^> holds

u * (f ") = v

A9: <^o1,o2^> <> {} by A2;

let v be Morphism of o2,o3; :: thesis: ( v in <^o2,o3^> implies u * (f ") = v )

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

v * f = u by A5, A6;

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