let G be Group; :: thesis: for A being Subset of G st ( 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

A * A = A

let A be Subset of G; :: thesis: ( ( 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 A * A = A )

assume that

A1: for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A and

A2: for g being Element of G st g in A holds

g " in A ; :: thesis: A * A = A

thus A * A c= A :: according to XBOOLE_0:def 10 :: thesis: A c= A * A

assume A3: x in A ; :: thesis: x in A * A

then reconsider a = x as Element of G ;

a " in A by A2, A3;

then (a ") * a in A by A1, A3;

then A4: 1_ G in A by GROUP_1:def 5;

(1_ G) * a = a by GROUP_1:def 4;

hence x in A * A by A3, A4; :: thesis: verum

g1 * g2 in A ) & ( for g being Element of G st g in A holds

g " in A ) holds

A * A = A

let A be Subset of G; :: thesis: ( ( 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 A * A = A )

assume that

A1: for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A and

A2: for g being Element of G st g in A holds

g " in A ; :: thesis: A * A = A

thus A * A c= A :: according to XBOOLE_0:def 10 :: thesis: A c= A * A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A * A )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A * A or x in A )

assume x in A * A ; :: thesis: x in A

then ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in A & g2 in A ) ;

hence x in A by A1; :: thesis: verum

end;assume x in A * A ; :: thesis: x in A

then ex g1, g2 being Element of G st

( x = g1 * g2 & g1 in A & g2 in A ) ;

hence x in A by A1; :: thesis: verum

assume A3: x in A ; :: thesis: x in A * A

then reconsider a = x as Element of G ;

a " in A by A2, A3;

then (a ") * a in A by A1, A3;

then A4: 1_ G in A by GROUP_1:def 5;

(1_ G) * a = a by GROUP_1:def 4;

hence x in A * A by A3, A4; :: thesis: verum