INT.Group n = multMagma(# (Segm n),(addint n) #) by A1, GR_CY_1:def 6;
hence h is Element of NAT by TARSKI:def 3; :: thesis: verum