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 2 :: thesis: for b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) holds
( b1 * t = b1 & t * b1 = b1 & ex b2 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( b1 * b2 = t & b2 * b1 = t ) )
let a be Element of multMagma(# the carrier of G, the multF of G #); :: thesis: ( a * t = a & t * a = a & ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( a * b1 = t & b1 * a = t ) )
reconsider x = a as Element of G ;
thus a * t = x * (1_ G)
.= a by GROUP_1:def 4 ; :: thesis: ( t * a = a & ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( a * b1 = t & b1 * a = t ) )
thus t * a = (1_ G) * x
.= a by GROUP_1:def 4 ; :: thesis: ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( a * b1 = t & b1 * 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 5 ; :: thesis: s * a = t
thus s * a = (x ") * x
.= t by GROUP_1:def 5 ; :: 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:19;
then H is Subgroup of G by Def5;
hence ex b1 being Subgroup of G st b1 is strict ; :: thesis: verum