let C be category; :: thesis: for o1, o2 being object of C st o1 is _zero & o2 is _zero holds
o1,o2 are_iso
let o1, o2 be object of C; :: thesis: ( o1 is _zero & o2 is _zero implies o1,o2 are_iso )
assume ( o1 is _zero & o2 is _zero ) ; :: thesis: o1,o2 are_iso
then ( o1 is initial & o2 is initial ) by Def11;
hence o1,o2 are_iso by Th26; :: thesis: verum