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

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