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

proof

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;

hence o2 is initial by ALTCAT_3:25; :: thesis: verum