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 ;
rng ( the multF of G || A) c= A
proof
let x be object ; :: 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 object 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 object such that
A8: [y1,y2] = y by ;
A9: ( y1 in A & y2 in A ) by ;
reconsider y1 = y1, y2 = y2 as Element of G by ;
x = y1 * y2 by ;
hence x in A by A2, A9; :: thesis: verum
end;
then reconsider o = the multF of G || A as BinOp of D by ;
set H = multMagma(# D,o #);
A10: now :: thesis: for g1, g2 being Element of G
for h1, h2 being Element of multMagma(# D,o #) st g1 = h1 & g2 = h2 holds
g1 * g2 = h1 * h2
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 ; :: 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 b1 being Element of the carrier of multMagma(# D,o #) holds
( b1 * t = b1 & t * b1 = b1 & ex b2 being Element of the carrier of multMagma(# D,o #) st
( b1 * b2 = t & b2 * b1 = t ) )

let a be Element of multMagma(# D,o #); :: thesis: ( a * t = a & t * a = a & ex b1 being Element of the carrier of multMagma(# D,o #) st
( a * b1 = t & b1 * 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 b1 being Element of the carrier of multMagma(# D,o #) st
( a * b1 = t & b1 * a = t ) )

thus t * a = (1_ G) * x by A10
.= a by GROUP_1:def 4 ; :: thesis: ex b1 being Element of the carrier of multMagma(# D,o #) st
( a * b1 = t & b1 * 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