let G be addGroup; :: thesis: for H1, H2 being Subgroup of G holds 0_ H1 = 0_ H2
let H1, H2 be Subgroup of G; :: thesis: 0_ H1 = 0_ H2
thus 0_ H1 = 0_ G by Th44
.= 0_ H2 by Th44 ; :: thesis: verum