let G be Group; :: thesis: for A being Subset of G st A = the carrier of G holds
gr A = multMagma(# the carrier of G, the multF of G #)
let A be Subset of G; :: thesis: ( A = the carrier of G implies gr A = multMagma(# the carrier of G, the multF of G #) )
assume A = the carrier of G ; :: thesis: gr A = multMagma(# the carrier of G, the multF of G #)
then the carrier of G c= the carrier of (gr A) by GROUP_4:def 4;
hence multMagma(# the carrier of G, the multF of G #) = gr A by GROUP_2:61; :: thesis: verum