take @' 1 ; :: according to GR_CY_1:def 7 :: thesis: multMagma(# the carrier of INT.Group, the multF of INT.Group #) = gr {(@' 1)}
thus multMagma(# the carrier of INT.Group, the multF of INT.Group #) = gr {(@' 1)} by Lm5; :: thesis: verum