let G be Group; :: thesis: for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g being Element of G st g in A holds
g " in A ) holds
ex H being strict Subgroup of G st the carrier of H = A
let A be Subset of G; :: thesis: ( A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g being Element of G st g in A holds
g " in A ) implies ex H being strict Subgroup of G st the carrier of H = A )
assume that
A1: A <> {} and
A2: for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A and
A3: for g being Element of G st g in A holds
g " in A ; :: thesis: ex H being strict Subgroup of G st the carrier of H = A
reconsider D = A as non empty set by A1;
set o = the multF of G || A;
A4: dom ( the multF of G || A) = (dom the multF of G) /\ [:A,A:] by RELAT_1:61;
dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def 1;
then A5: dom ( the multF of G || A) = [:A,A:] by A4, XBOOLE_1:28;
rng ( the multF of G || A) c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ( the multF of G || A) or x in A )
assume x in rng ( the multF of G || A) ; :: thesis: x in A
then consider y being set such that
A6: y in dom ( the multF of G || A) and
A7: ( the multF of G || A) . y = x by FUNCT_1:def 3;
consider y1, y2 being set such that
A8: [y1,y2] = y by A4, A6, RELAT_1:def 1;
A9: ( y1 in A & y2 in A ) by A5, A6, A8, ZFMISC_1:87;
reconsider y1 = y1, y2 = y2 as Element of G by A4, A6, A8, ZFMISC_1:87;
x = y1 * y2 by A6, A7, A8, FUNCT_1:47;
hence x in A by A2, A9; :: thesis: verum

end;

then reconsider o = the multF of G || A as BinOp of D by A5, FUNCT_2:def 1, RELSET_1:4;
set H = multMagma(# D,o #);

A10: now

let g1, g2 be Element of G; :: thesis: for h1, h2 being Element of multMagma(# D,o #) st g1 = h1 & g2 = h2 holds
g1 * g2 = h1 * h2
let h1, h2 be Element of multMagma(# D,o #); :: thesis: ( g1 = h1 & g2 = h2 implies g1 * g2 = h1 * h2 )
A11: h1 * h2 = ( the multF of G || A) . [h1,h2] ;
assume ( g1 = h1 & g2 = h2 ) ; :: thesis: g1 * g2 = h1 * h2
hence g1 * g2 = h1 * h2 by A11, FUNCT_1:49; :: thesis: verum

end;

multMagma(# D,o #) is Group-like

proof

set a = the Element of multMagma(# D,o #);
reconsider x = the Element of multMagma(# D,o #) as Element of G by Lm1;
x " in A by A3;
then x * (x ") in A by A2;
then reconsider t = 1_ G as Element of multMagma(# D,o #) by GROUP_1:def 5;
take t ; :: according to GROUP_1:def 2 :: thesis: for b₁ being Element of the carrier of multMagma(# D,o #) holds
( b₁ * t = b₁ & t * b₁ = b₁ & ex b₂ being Element of the carrier of multMagma(# D,o #) st
( b₁ * b₂ = t & b₂ * b₁ = t ) )
let a be Element of multMagma(# D,o #); :: thesis: ( a * t = a & t * a = a & ex b₁ being Element of the carrier of multMagma(# D,o #) st
( a * b₁ = t & b₁ * a = t ) )
reconsider x = a as Element of G by Lm1;
thus a * t = x * (1_ G) by A10
.= a by GROUP_1:def 4 ; :: thesis: ( t * a = a & ex b₁ being Element of the carrier of multMagma(# D,o #) st
( a * b₁ = t & b₁ * a = t ) )
thus t * a = (1_ G) * x by A10
.= a by GROUP_1:def 4 ; :: thesis: ex b₁ being Element of the carrier of multMagma(# D,o #) st
( a * b₁ = t & b₁ * a = t )
reconsider s = x " as Element of multMagma(# D,o #) by A3;
take s ; :: thesis: ( a * s = t & s * a = t )
thus a * s = x * (x ") by A10
.= t by GROUP_1:def 5 ; :: thesis: s * a = t
thus s * a = (x ") * x by A10
.= t by GROUP_1:def 5 ; :: thesis: verum

end;

then reconsider H = multMagma(# D,o #) as non empty Group-like multMagma ;
reconsider H = H as strict Subgroup of G by Def5;
take H ; :: thesis: the carrier of H = A
thus the carrier of H = A ; :: thesis: verum