for Gc being cyclic Group
for H being Subgroup of Gc
for g being Element of Gc st Gc = gr {g} & g in H holds
multMagma(# the carrier of Gc, the multF of Gc #) = multMagma(# the carrier of H, the multF of H #)