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

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
A3: u in <^o1,o3^> and
A4: for M1 being Morphism of o1,o3 st M1 in <^o1,o3^> holds
u = M1 by A1, ALTCAT_3:25;
consider f being Morphism of o1,o2 such that
A5: f is iso by A2, ALTCAT_3:def 6;
A6: f * (f " ) = idm o2 by A5, ALTCAT_3:def 5;
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: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A2, ALTCAT_3:def 6;
then A8: <^o2,o3^> <> {} by A3, ALTCAT_1:def 4;
hence u * (f " ) in <^o2,o3^> ; :: thesis: for v being Morphism of o2,o3 st v in <^o2,o3^> holds
u * (f " ) = v
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 A3, A4;
hence u * (f " ) = v by A6, A7, A8, Th2; :: thesis: verum

end;

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