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

set H = multMagma(# D,o #);

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

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

then reconsider o = the multF of G || A as BinOp of D by A5, FUNCT_2:def 1, RELSET_1:4;
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 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;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 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

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

multMagma(# D,o #) is Group-like
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 A11, FUNCT_1:49; :: thesis: verum

end;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

proof

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

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

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

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

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

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

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

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

( a * b_{1} = t & b_{1} * 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;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

( b

( b

let a be Element of multMagma(# D,o #); :: thesis: ( a * t = a & t * a = a & ex b

( a * b

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

( a * b

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

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

( a * b

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

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