set H = multMagma(# the carrier of G,the multF of G #);
multMagma(# the carrier of G,the multF of G #) is Group-like

proof

reconsider t = 1_ G as Element of multMagma(# the carrier of G,the multF of G #) ;
take t ; :: according to GROUP_1:def 3 :: thesis: for b₁ being Element of the carrier of multMagma(# the carrier of G,the multF of G #) holds
( b₁ * t = b₁ & t * b₁ = b₁ & ex b₂ being Element of the carrier of multMagma(# the carrier of G,the multF of G #) st
( b₁ * b₂ = t & b₂ * b₁ = t ) )
let a be Element of multMagma(# the carrier of G,the multF of G #); :: thesis: ( a * t = a & t * a = a & ex b₁ being Element of the carrier of multMagma(# the carrier of G,the multF of G #) st
( a * b₁ = t & b₁ * a = t ) )
reconsider x = a as Element of G ;
thus a * t = x * (1_ G)
.= a by GROUP_1:def 5 ; :: thesis: ( t * a = a & ex b₁ being Element of the carrier of multMagma(# the carrier of G,the multF of G #) st
( a * b₁ = t & b₁ * a = t ) )
thus t * a = (1_ G) * x
.= a by GROUP_1:def 5 ; :: thesis: ex b₁ being Element of the carrier of multMagma(# the carrier of G,the multF of G #) st
( a * b₁ = t & b₁ * a = t )
reconsider s = x " as Element of multMagma(# the carrier of G,the multF of G #) ;
take s ; :: thesis: ( a * s = t & s * a = t )
thus a * s = x * (x " )
.= t by GROUP_1:def 6 ; :: thesis: s * a = t
thus s * a = (x " ) * x
.= t by GROUP_1:def 6 ; :: thesis: verum

end;

then reconsider H = multMagma(# the carrier of G,the multF of G #) as non empty Group-like multMagma ;
the multF of H = the multF of G || the carrier of H by RELSET_1:34;
then H is Subgroup of G by Def5;
hence ex b₁ being Subgroup of G st b₁ is strict ; :: thesis: verum