set H = multMagma(# the carrier of G, the multF of G #);

multMagma(# the carrier of G, the multF of G #) is Group-like

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 b_{1} being Subgroup of G st b_{1} is strict
; :: thesis: verum

multMagma(# the carrier of G, the multF of G #) is Group-like

proof

then reconsider H = multMagma(# the carrier of G, the multF of G #) as non empty Group-like multMagma ;
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 b_{1} being Element of the carrier of multMagma(# the carrier of G, the multF of G #) holds

( b_{1} * t = b_{1} & t * b_{1} = b_{1} & ex b_{2} being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st

( b_{1} * b_{2} = t & b_{2} * b_{1} = t ) )

let a be Element of multMagma(# the carrier of G, the multF of G #); :: thesis: ( a * t = a & t * a = a & ex b_{1} being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st

( a * b_{1} = t & b_{1} * 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 b_{1} being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st

( a * b_{1} = t & b_{1} * a = t ) )

thus t * a = (1_ G) * x

.= a by GROUP_1:def 4 ; :: thesis: ex b_{1} being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st

( a * b_{1} = t & b_{1} * 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;take t ; :: according to GROUP_1:def 2 :: thesis: for b

( b

( b

let a be Element of multMagma(# the carrier of G, the multF of G #); :: thesis: ( a * t = a & t * a = a & ex b

( a * b

reconsider x = a as Element of G ;

thus a * t = x * (1_ G)

.= a by GROUP_1:def 4 ; :: thesis: ( t * a = a & ex b

( a * b

thus t * a = (1_ G) * x

.= a by GROUP_1:def 4 ; :: thesis: ex b

( a * b

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

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 b