let n be non zero Nat; :: thesis: the multF of (INT.Group n) = addint n
thus the multF of (INT.Group n) = the multF of multMagma(# (Segm n),(addint n) #) by GR_CY_1:def 5
.= addint n ; :: thesis: verum