let G be Group; :: thesis: for H being Subgroup of G holds multMagma(# the carrier of H, the multF of H #) is strict Subgroup of G
let H be Subgroup of G; :: thesis: multMagma(# the carrier of H, the multF of H #) is strict Subgroup of G
set H0 = multMagma(# the carrier of H, the multF of H #);
( the carrier of multMagma(# the carrier of H, the multF of H #) c= the carrier of G & the multF of multMagma(# the carrier of H, the multF of H #) = the multF of G || the carrier of multMagma(# the carrier of H, the multF of H #) ) by GROUP_2:def 5;
hence multMagma(# the carrier of H, the multF of H #) is strict Subgroup of G by GROUP_2:def 5; :: thesis: verum