let Gc be cyclic Group; :: thesis: 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 #)
let H be Subgroup of Gc; :: thesis: 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 #)
let g be Element of Gc; :: thesis: ( Gc = gr {g} & g in H implies multMagma(# the carrier of Gc, the multF of Gc #) = multMagma(# the carrier of H, the multF of H #) )
assume that
A1: Gc = gr {g} and
A2: g in H ; :: thesis: multMagma(# the carrier of Gc, the multF of Gc #) = multMagma(# the carrier of H, the multF of H #)
reconsider g9 = g as Element of H by A2, STRUCT_0:def 5;
gr {g9} is Subgroup of H ;
then gr {g} is Subgroup of H by Th3;
hence multMagma(# the carrier of Gc, the multF of Gc #) = multMagma(# the carrier of H, the multF of H #) by A1, GROUP_2:55; :: thesis: verum