let G be addGroup; :: thesis: for H being Subgroup of G holds 0_ H = 0_ G
let H be Subgroup of G; :: thesis: 0_ H = 0_ G
set h = the Element of H;
reconsider g = the Element of H, g9 = 0_ H as Element of G by Th41, STRUCT_0:def 5;
the Element of H + (0_ H) = the Element of H by Def4;
then g + g9 = g by Th43;
hence 0_ H = 0_ G by Th7; :: thesis: verum