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, ALTCAT_3:def 6;
A4: f * (f ") = idm o2 by A3, ALTCAT_3:def 5;
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, ALTCAT_3:def 6;
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, ALTCAT_3:def 6;
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