INT.Group n = multMagma(# (Segm n),(addint n) #) by Def6;
hence the carrier of (INT.Group n) is finite ; :: according to STRUCT_0:def 11 :: thesis: verum