:: GROUP_2 semantic presentation

begin

   Lm1:  for x being set
for G being non empty 1-sorted
for A being Subset of G st x in A holds
x is Element of G
;

theorem :: GROUP_2:1
for G being non empty 1-sorted
for A being Subset of G st G is finite holds
A is finite ;


definition
let G be Group;
let A be Subset of G;
funcA "  ->  Subset of G equals :: GROUP_2:def 1
 {  (g ") where g is Element of G : g in A  }  ;
coherence
  {  (g ") where g is Element of G : g in A  }  is Subset of G
proof
set F =  {  (g ") where g is Element of G : g in A  }  ;
  {  (g ") where g is Element of G : g in A  }  c= the carrier of G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (g ") where g is Element of G : g in A  }  or x in the carrier of G )
assume  x in  {  (g ") where g is Element of G : g in A  }  ; ::_thesis: x in the carrier of G
then  ex g being Element of G st
( x = g " & g in A ) ;
hence  x in the carrier of G ; ::_thesis: verum
end;
hence   {  (g ") where g is Element of G : g in A  }  is Subset of G ; ::_thesis: verum
end;
involutiveness
 for b1, b2 being Subset of G st b1 =  {  (g ") where g is Element of G : g in b2  }  holds
b2 =  {  (g ") where g is Element of G : g in b1  }
proof
let R, B be Subset of G; ::_thesis: ( R =  {  (g ") where g is Element of G : g in B  }  implies B =  {  (g ") where g is Element of G : g in R  }  )
assume A1: R =  {  (g ") where g is Element of G : g in B  }  ; ::_thesis: B =  {  (g ") where g is Element of G : g in R  }
thus  B c=  {  (g ") where g is Element of G : g in R  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (g ") where g is Element of G : g in R  }  c= B
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in  {  (g ") where g is Element of G : g in R  }  )
assume A2: a in B ; ::_thesis: a in  {  (g ") where g is Element of G : g in R  }
then reconsider a = a as Element of G ;
 ( (a ") " = a & a " in R ) by A1, A2;
hence  a in  {  (g ") where g is Element of G : g in R  }  ; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (g ") where g is Element of G : g in R  }  or a in B )
assume  a in  {  (g ") where g is Element of G : g in R  }  ; ::_thesis: a in B
then consider g being Element of G such that
A3: a = g " and
A4: g in R ;
 ex h being Element of G st
( g = h " & h in B ) by A1, A4;
hence  a in B by A3; ::_thesis: verum
end;
end;

:: deftheorem  defines " GROUP_2:def_1_:_
 for G being Group
for A being Subset of G holds A " =  {  (g ") where g is Element of G : g in A  }  ;

theorem Th2: :: GROUP_2:2
for x being set
for G being Group
for A being Subset of G holds
( x in A " iff ex g being Element of G st
( x = g " & g in A ) ) ;

theorem :: GROUP_2:3
for G being Group
for g being Element of G holds {g} " = {(g ")}
proof
let G be Group; ::_thesis: for g being Element of G holds {g} " = {(g ")}
let g be Element of G; ::_thesis: {g} " = {(g ")}
thus  {g} " c= {(g ")} :: according to XBOOLE_0:def_10 ::_thesis: {(g ")} c= {g} "
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {g} " or x in {(g ")} )
assume  x in {g} " ; ::_thesis: x in {(g ")}
then consider h being Element of G such that
A1: x = h " and
A2: h in {g} ;
 h = g by A2, TARSKI:def_1;
hence  x in {(g ")} by A1, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g ")} or x in {g} " )
assume  x in {(g ")} ; ::_thesis: x in {g} "
then A3: x = g " by TARSKI:def_1;
 g in {g} by TARSKI:def_1;
hence  x in {g} " by A3; ::_thesis: verum
end;

theorem :: GROUP_2:4
for G being Group
for g, h being Element of G holds {g,h} " = {(g "),(h ")}
proof
let G be Group; ::_thesis: for g, h being Element of G holds {g,h} " = {(g "),(h ")}
let g, h be Element of G; ::_thesis: {g,h} " = {(g "),(h ")}
thus  {g,h} " c= {(g "),(h ")} :: according to XBOOLE_0:def_10 ::_thesis: {(g "),(h ")} c= {g,h} "
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {g,h} " or x in {(g "),(h ")} )
assume  x in {g,h} " ; ::_thesis: x in {(g "),(h ")}
then consider a being Element of G such that
A1: x = a " and
A2: a in {g,h} ;
 ( a = g or a = h ) by A2, TARSKI:def_2;
hence  x in {(g "),(h ")} by A1, TARSKI:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g "),(h ")} or x in {g,h} " )
assume  x in {(g "),(h ")} ; ::_thesis: x in {g,h} "
then A3: ( x = g " or x = h " ) by TARSKI:def_2;
 ( g in {g,h} & h in {g,h} ) by TARSKI:def_2;
hence  x in {g,h} " by A3; ::_thesis: verum
end;

theorem :: GROUP_2:5
for G being Group holds ({} the carrier of G) " = {}
proof
let G be Group; ::_thesis: ({} the carrier of G) " = {}
thus  ({} the carrier of G) " c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= ({} the carrier of G) "
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ({} the carrier of G) " or x in {} )
assume  x in ({} the carrier of G) " ; ::_thesis: x in {}
then  ex a being Element of G st
( x = a " & a in {} the carrier of G ) ;
hence  x in {} ; ::_thesis: verum
end;
thus  {} c= ({} the carrier of G) " by XBOOLE_1:2; ::_thesis: verum
end;

theorem :: GROUP_2:6
for G being Group holds ([#] the carrier of G) " = the carrier of G
proof
let G be Group; ::_thesis: ([#] the carrier of G) " = the carrier of G
thus  ([#] the carrier of G) " c= the carrier of G ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of G c= ([#] the carrier of G) "
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of G or x in ([#] the carrier of G) " )
assume  x in the carrier of G ; ::_thesis: x in ([#] the carrier of G) "
then reconsider a = x as Element of G ;
 (a ") " in ([#] the carrier of G) " ;
hence  x in ([#] the carrier of G) " ; ::_thesis: verum
end;

theorem Th7: :: GROUP_2:7
for G being Group
for A being Subset of G holds
( A <> {} iff A " <> {} )
proof
let G be Group; ::_thesis: for A being Subset of G holds
( A <> {} iff A " <> {} )
let A be Subset of G; ::_thesis: ( A <> {} iff A " <> {} )
set x = the Element of A " ;
thus  ( A <> {} implies A " <> {} ) ::_thesis: ( A " <> {} implies A <> {} )
proof
set x = the Element of A;
assume A1: A <> {} ; ::_thesis: A " <> {}
then reconsider x = the Element of A as Element of G by Lm1;
 x " in A " by A1;
hence  A " <> {} ; ::_thesis: verum
end;
assume  A " <> {} ; ::_thesis: A <> {}
then  ex a being Element of G st
( the Element of A " = a " & a in A ) by Th2;
hence  A <> {} ; ::_thesis: verum
end;

registration
let G be Group;
let A be empty Subset of G;
clusterA "  ->  empty ;
coherence
 A " is empty by Th7;
end;

registration
let G be Group;
let A be non empty Subset of G;
clusterA "  ->  non empty ;
coherence
 not A " is empty by Th7;
end;


definition
let G be non empty multMagma ;
let A, B be Subset of G;
funcA * B ->  Subset of G equals :: GROUP_2:def 2
 {  (g * h) where g, h is Element of G : ( g in A & h in B )  }  ;
coherence
  {  (g * h) where g, h is Element of G : ( g in A & h in B )  }  is Subset of G
proof
set S =  {  (g * h) where g, h is Element of G : ( g in A & h in B )  }  ;
  {  (g * h) where g, h is Element of G : ( g in A & h in B )  }  c= the carrier of G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (g * h) where g, h is Element of G : ( g in A & h in B )  }  or x in the carrier of G )
assume  x in  {  (g * h) where g, h is Element of G : ( g in A & h in B )  }  ; ::_thesis: x in the carrier of G
then  ex g, h being Element of G st
( x = g * h & g in A & h in B ) ;
hence  x in the carrier of G ; ::_thesis: verum
end;
hence   {  (g * h) where g, h is Element of G : ( g in A & h in B )  }  is Subset of G ; ::_thesis: verum
end;
end;

:: deftheorem  defines * GROUP_2:def_2_:_
 for G being non empty multMagma
for A, B being Subset of G holds A * B =  {  (g * h) where g, h is Element of G : ( g in A & h in B )  }  ;

definition
let G be non empty commutative multMagma ;
let A, B be Subset of G;
:: original: *
redefine funcA * B ->  Subset of G;
commutativity
 for A, B being Subset of G holds A * B = B * A
proof
let A, B be Subset of G; ::_thesis: A * B = B * A
thus  A * B c= B * A :: according to XBOOLE_0:def_10 ::_thesis: B * A c= A * B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * B or x in B * A )
assume  x in A * B ; ::_thesis: x in B * A
then  ex g, h being Element of G st
( x = g * h & g in A & h in B ) ;
hence  x in B * A ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B * A or x in A * B )
assume  x in B * A ; ::_thesis: x in A * B
then  ex g, h being Element of G st
( x = g * h & g in B & h in A ) ;
hence  x in A * B ; ::_thesis: verum
end;
end;

theorem Th8: :: GROUP_2:8
for x being set
for G being non empty multMagma
for A, B being Subset of G holds
( x in A * B iff ex g, h being Element of G st
( x = g * h & g in A & h in B ) ) ;

theorem Th9: :: GROUP_2:9
for G being non empty multMagma
for A, B being Subset of G holds
( ( A <> {} & B <> {} ) iff A * B <> {} )
proof
let G be non empty multMagma ; ::_thesis: for A, B being Subset of G holds
( ( A <> {} & B <> {} ) iff A * B <> {} )
let A, B be Subset of G; ::_thesis: ( ( A <> {} & B <> {} ) iff A * B <> {} )
thus  ( A <> {} & B <> {} implies A * B <> {} ) ::_thesis: ( A * B <> {} implies ( A <> {} & B <> {} ) )
proof
assume A1: A <> {} ; ::_thesis: ( not B <> {} or A * B <> {} )
then reconsider x = the Element of A as Element of G by TARSKI:def_3;
assume A2: B <> {} ; ::_thesis: A * B <> {}
then reconsider y = the Element of B as Element of G by TARSKI:def_3;
 x * y in A * B by A1, A2;
hence  A * B <> {} ; ::_thesis: verum
end;
set x = the Element of A * B;
assume  A * B <> {} ; ::_thesis: ( A <> {} & B <> {} )
then  ex a, b being Element of G st
( the Element of A * B = a * b & a in A & b in B ) by Th8;
hence  ( A <> {} & B <> {} ) ; ::_thesis: verum
end;

theorem Th10: :: GROUP_2:10
for G being non empty multMagma
for A, B, C being Subset of G st G is associative holds
(A * B) * C = A * (B * C)
proof
let G be non empty multMagma ; ::_thesis: for A, B, C being Subset of G st G is associative holds
(A * B) * C = A * (B * C)
let A, B, C be Subset of G; ::_thesis: ( G is associative implies (A * B) * C = A * (B * C) )
assume A1: G is associative ; ::_thesis: (A * B) * C = A * (B * C)
thus  (A * B) * C c= A * (B * C) :: according to XBOOLE_0:def_10 ::_thesis: A * (B * C) c= (A * B) * C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A * B) * C or x in A * (B * C) )
assume  x in (A * B) * C ; ::_thesis: x in A * (B * C)
then consider g, h being Element of G such that
A2: x = g * h and
A3: g in A * B and
A4: h in C ;
consider g1, g2 being Element of G such that
A5: g = g1 * g2 and
A6: g1 in A and
A7: g2 in B by A3;
 ( x = g1 * (g2 * h) & g2 * h in B * C ) by A1, A2, A4, A5, A7, GROUP_1:def_3;
hence  x in A * (B * C) by A6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * (B * C) or x in (A * B) * C )
assume  x in A * (B * C) ; ::_thesis: x in (A * B) * C
then consider g, h being Element of G such that
A8: x = g * h and
A9: g in A and
A10: h in B * C ;
consider g1, g2 being Element of G such that
A11: h = g1 * g2 and
A12: g1 in B and
A13: g2 in C by A10;
A14: g * g1 in A * B by A9, A12;
 x = (g * g1) * g2 by A1, A8, A11, GROUP_1:def_3;
hence  x in (A * B) * C by A13, A14; ::_thesis: verum
end;

theorem :: GROUP_2:11
for G being Group
for A, B being Subset of G holds (A * B) " = (B ") * (A ")
proof
let G be Group; ::_thesis: for A, B being Subset of G holds (A * B) " = (B ") * (A ")
let A, B be Subset of G; ::_thesis: (A * B) " = (B ") * (A ")
thus  (A * B) " c= (B ") * (A ") :: according to XBOOLE_0:def_10 ::_thesis: (B ") * (A ") c= (A * B) "
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A * B) " or x in (B ") * (A ") )
assume  x in (A * B) " ; ::_thesis: x in (B ") * (A ")
then consider g being Element of G such that
A1: x = g " and
A2: g in A * B ;
consider g1, g2 being Element of G such that
A3: g = g1 * g2 and
A4: ( g1 in A & g2 in B ) by A2;
A5: ( g1 " in A " & g2 " in B " ) by A4;
 x = (g2 ") * (g1 ") by A1, A3, GROUP_1:17;
hence  x in (B ") * (A ") by A5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B ") * (A ") or x in (A * B) " )
assume  x in (B ") * (A ") ; ::_thesis: x in (A * B) "
then consider g1, g2 being Element of G such that
A6: x = g1 * g2 and
A7: g1 in B " and
A8: g2 in A " ;
consider b being Element of G such that
A9: g2 = b " and
A10: b in A by A8;
consider a being Element of G such that
A11: g1 = a " and
A12: a in B by A7;
A13: b * a in A * B by A12, A10;
 x = (b * a) " by A6, A11, A9, GROUP_1:17;
hence  x in (A * B) " by A13; ::_thesis: verum
end;

theorem :: GROUP_2:12
for G being non empty multMagma
for A, B, C being Subset of G holds A * (B \/ C) = (A * B) \/ (A * C)
proof
let G be non empty multMagma ; ::_thesis: for A, B, C being Subset of G holds A * (B \/ C) = (A * B) \/ (A * C)
let A, B, C be Subset of G; ::_thesis: A * (B \/ C) = (A * B) \/ (A * C)
thus  A * (B \/ C) c= (A * B) \/ (A * C) :: according to XBOOLE_0:def_10 ::_thesis: (A * B) \/ (A * C) c= A * (B \/ C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * (B \/ C) or x in (A * B) \/ (A * C) )
assume  x in A * (B \/ C) ; ::_thesis: x in (A * B) \/ (A * C)
then consider g1, g2 being Element of G such that
A1: ( x = g1 * g2 & g1 in A ) and
A2: g2 in B \/ C ;
 ( g2 in B or g2 in C ) by A2, XBOOLE_0:def_3;
then  ( x in A * B or x in A * C ) by A1;
hence  x in (A * B) \/ (A * C) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A * B) \/ (A * C) or x in A * (B \/ C) )
assume A3: x in (A * B) \/ (A * C) ; ::_thesis: x in A * (B \/ C)
now__::_thesis:_x_in_A_*_(B_\/_C)
percases ( x in A * B or x in A * C ) by A3, XBOOLE_0:def_3;
suppose x in A * B ; ::_thesis: x in A * (B \/ C)
then consider g1, g2 being Element of G such that
A4: ( x = g1 * g2 & g1 in A ) and
A5: g2 in B ;
 g2 in B \/ C by A5, XBOOLE_0:def_3;
hence  x in A * (B \/ C) by A4; ::_thesis: verum
end;
suppose x in A * C ; ::_thesis: x in A * (B \/ C)
then consider g1, g2 being Element of G such that
A6: ( x = g1 * g2 & g1 in A ) and
A7: g2 in C ;
 g2 in B \/ C by A7, XBOOLE_0:def_3;
hence  x in A * (B \/ C) by A6; ::_thesis: verum
end;
end;
end;
hence  x in A * (B \/ C) ; ::_thesis: verum
end;

theorem :: GROUP_2:13
for G being non empty multMagma
for A, B, C being Subset of G holds (A \/ B) * C = (A * C) \/ (B * C)
proof
let G be non empty multMagma ; ::_thesis: for A, B, C being Subset of G holds (A \/ B) * C = (A * C) \/ (B * C)
let A, B, C be Subset of G; ::_thesis: (A \/ B) * C = (A * C) \/ (B * C)
thus  (A \/ B) * C c= (A * C) \/ (B * C) :: according to XBOOLE_0:def_10 ::_thesis: (A * C) \/ (B * C) c= (A \/ B) * C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A \/ B) * C or x in (A * C) \/ (B * C) )
assume  x in (A \/ B) * C ; ::_thesis: x in (A * C) \/ (B * C)
then consider g1, g2 being Element of G such that
A1: x = g1 * g2 and
A2: g1 in A \/ B and
A3: g2 in C ;
 ( g1 in A or g1 in B ) by A2, XBOOLE_0:def_3;
then  ( x in A * C or x in B * C ) by A1, A3;
hence  x in (A * C) \/ (B * C) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A * C) \/ (B * C) or x in (A \/ B) * C )
assume A4: x in (A * C) \/ (B * C) ; ::_thesis: x in (A \/ B) * C
now__::_thesis:_x_in_(A_\/_B)_*_C
percases ( x in A * C or x in B * C ) by A4, XBOOLE_0:def_3;
suppose x in A * C ; ::_thesis: x in (A \/ B) * C
then consider g1, g2 being Element of G such that
A5: x = g1 * g2 and
A6: g1 in A and
A7: g2 in C ;
 g1 in A \/ B by A6, XBOOLE_0:def_3;
hence  x in (A \/ B) * C by A5, A7; ::_thesis: verum
end;
suppose x in B * C ; ::_thesis: x in (A \/ B) * C
then consider g1, g2 being Element of G such that
A8: x = g1 * g2 and
A9: g1 in B and
A10: g2 in C ;
 g1 in A \/ B by A9, XBOOLE_0:def_3;
hence  x in (A \/ B) * C by A8, A10; ::_thesis: verum
end;
end;
end;
hence  x in (A \/ B) * C ; ::_thesis: verum
end;

theorem :: GROUP_2:14
for G being non empty multMagma
for A, B, C being Subset of G holds A * (B /\ C) c= (A * B) /\ (A * C)
proof
let G be non empty multMagma ; ::_thesis: for A, B, C being Subset of G holds A * (B /\ C) c= (A * B) /\ (A * C)
let A, B, C be Subset of G; ::_thesis: A * (B /\ C) c= (A * B) /\ (A * C)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * (B /\ C) or x in (A * B) /\ (A * C) )
assume  x in A * (B /\ C) ; ::_thesis: x in (A * B) /\ (A * C)
then consider g1, g2 being Element of G such that
A1: ( x = g1 * g2 & g1 in A ) and
A2: g2 in B /\ C ;
 g2 in C by A2, XBOOLE_0:def_4;
then A3: x in A * C by A1;
 g2 in B by A2, XBOOLE_0:def_4;
then  x in A * B by A1;
hence  x in (A * B) /\ (A * C) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: GROUP_2:15
for G being non empty multMagma
for A, B, C being Subset of G holds (A /\ B) * C c= (A * C) /\ (B * C)
proof
let G be non empty multMagma ; ::_thesis: for A, B, C being Subset of G holds (A /\ B) * C c= (A * C) /\ (B * C)
let A, B, C be Subset of G; ::_thesis: (A /\ B) * C c= (A * C) /\ (B * C)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A /\ B) * C or x in (A * C) /\ (B * C) )
assume  x in (A /\ B) * C ; ::_thesis: x in (A * C) /\ (B * C)
then consider g1, g2 being Element of G such that
A1: x = g1 * g2 and
A2: g1 in A /\ B and
A3: g2 in C ;
 g1 in B by A2, XBOOLE_0:def_4;
then A4: x in B * C by A1, A3;
 g1 in A by A2, XBOOLE_0:def_4;
then  x in A * C by A1, A3;
hence  x in (A * C) /\ (B * C) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th16: :: GROUP_2:16
for G being non empty multMagma
for A being Subset of G holds
( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} )
proof
let G be non empty multMagma ; ::_thesis: for A being Subset of G holds
( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} )
let A be Subset of G; ::_thesis: ( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} )
A1: now__::_thesis:_not_A_*_({}_the_carrier_of_G)_<>_{}
set x = the Element of A * ({} the carrier of G);
assume  A * ({} the carrier of G) <> {} ; ::_thesis: contradiction
then  ex g1, g2 being Element of G st
( the Element of A * ({} the carrier of G) = g1 * g2 & g1 in A & g2 in {} the carrier of G ) by Th8;
hence  contradiction ; ::_thesis: verum
end;
now__::_thesis:_not_({}_the_carrier_of_G)_*_A_<>_{}
set x = the Element of ({} the carrier of G) * A;
assume  ({} the carrier of G) * A <> {} ; ::_thesis: contradiction
then  ex g1, g2 being Element of G st
( the Element of ({} the carrier of G) * A = g1 * g2 & g1 in {} the carrier of G & g2 in A ) by Th8;
hence  contradiction ; ::_thesis: verum
end;
hence  ( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} ) by A1; ::_thesis: verum
end;

theorem Th17: :: GROUP_2:17
for G being Group
for A being Subset of G st A <> {} holds
( ([#] the carrier of G) * A = the carrier of G & A * ([#] the carrier of G) = the carrier of G )
proof
let G be Group; ::_thesis: for A being Subset of G st A <> {} holds
( ([#] the carrier of G) * A = the carrier of G & A * ([#] the carrier of G) = the carrier of G )
let A be Subset of G; ::_thesis: ( A <> {} implies ( ([#] the carrier of G) * A = the carrier of G & A * ([#] the carrier of G) = the carrier of G ) )
set y = the Element of A;
assume A1: A <> {} ; ::_thesis: ( ([#] the carrier of G) * A = the carrier of G & A * ([#] the carrier of G) = the carrier of G )
then reconsider y = the Element of A as Element of G by Lm1;
thus  ([#] the carrier of G) * A = the carrier of G ::_thesis: A * ([#] the carrier of G) = the carrier of G
proof
set y = the Element of A;
reconsider y = the Element of A as Element of G by A1, Lm1;
thus  ([#] the carrier of G) * A c= the carrier of G ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of G c= ([#] the carrier of G) * A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of G or x in ([#] the carrier of G) * A )
assume  x in the carrier of G ; ::_thesis: x in ([#] the carrier of G) * A
then reconsider a = x as Element of G ;
(a * (y ")) * y = a * ((y ") * y) by GROUP_1:def_3
.= a * (1_ G) by GROUP_1:def_5
.= a by GROUP_1:def_4 ;
hence  x in ([#] the carrier of G) * A by A1; ::_thesis: verum
end;
thus  A * ([#] the carrier of G) c= the carrier of G ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of G c= A * ([#] the carrier of G)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of G or x in A * ([#] the carrier of G) )
assume  x in the carrier of G ; ::_thesis: x in A * ([#] the carrier of G)
then reconsider a = x as Element of G ;
y * ((y ") * a) = (y * (y ")) * a by GROUP_1:def_3
.= (1_ G) * a by GROUP_1:def_5
.= a by GROUP_1:def_4 ;
hence  x in A * ([#] the carrier of G) by A1; ::_thesis: verum
end;

theorem Th18: :: GROUP_2:18
for G being non empty multMagma
for g, h being Element of G holds {g} * {h} = {(g * h)}
proof
let G be non empty multMagma ; ::_thesis: for g, h being Element of G holds {g} * {h} = {(g * h)}
let g, h be Element of G; ::_thesis: {g} * {h} = {(g * h)}
thus  {g} * {h} c= {(g * h)} :: according to XBOOLE_0:def_10 ::_thesis: {(g * h)} c= {g} * {h}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {g} * {h} or x in {(g * h)} )
assume  x in {g} * {h} ; ::_thesis: x in {(g * h)}
then consider g1, g2 being Element of G such that
A1: x = g1 * g2 and
A2: ( g1 in {g} & g2 in {h} ) ;
 ( g1 = g & g2 = h ) by A2, TARSKI:def_1;
hence  x in {(g * h)} by A1, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g * h)} or x in {g} * {h} )
assume  x in {(g * h)} ; ::_thesis: x in {g} * {h}
then A3: x = g * h by TARSKI:def_1;
 ( g in {g} & h in {h} ) by TARSKI:def_1;
hence  x in {g} * {h} by A3; ::_thesis: verum
end;

theorem :: GROUP_2:19
for G being non empty multMagma
for g, g1, g2 being Element of G holds {g} * {g1,g2} = {(g * g1),(g * g2)}
proof
let G be non empty multMagma ; ::_thesis: for g, g1, g2 being Element of G holds {g} * {g1,g2} = {(g * g1),(g * g2)}
let g, g1, g2 be Element of G; ::_thesis: {g} * {g1,g2} = {(g * g1),(g * g2)}
thus  {g} * {g1,g2} c= {(g * g1),(g * g2)} :: according to XBOOLE_0:def_10 ::_thesis: {(g * g1),(g * g2)} c= {g} * {g1,g2}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {g} * {g1,g2} or x in {(g * g1),(g * g2)} )
assume  x in {g} * {g1,g2} ; ::_thesis: x in {(g * g1),(g * g2)}
then consider h1, h2 being Element of G such that
A1: x = h1 * h2 and
A2: h1 in {g} and
A3: h2 in {g1,g2} ;
A4: ( h2 = g1 or h2 = g2 ) by A3, TARSKI:def_2;
 h1 = g by A2, TARSKI:def_1;
hence  x in {(g * g1),(g * g2)} by A1, A4, TARSKI:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g * g1),(g * g2)} or x in {g} * {g1,g2} )
A5: g2 in {g1,g2} by TARSKI:def_2;
assume  x in {(g * g1),(g * g2)} ; ::_thesis: x in {g} * {g1,g2}
then A6: ( x = g * g1 or x = g * g2 ) by TARSKI:def_2;
 ( g in {g} & g1 in {g1,g2} ) by TARSKI:def_1, TARSKI:def_2;
hence  x in {g} * {g1,g2} by A6, A5; ::_thesis: verum
end;

theorem :: GROUP_2:20
for G being non empty multMagma
for g1, g2, g being Element of G holds {g1,g2} * {g} = {(g1 * g),(g2 * g)}
proof
let G be non empty multMagma ; ::_thesis: for g1, g2, g being Element of G holds {g1,g2} * {g} = {(g1 * g),(g2 * g)}
let g1, g2, g be Element of G; ::_thesis: {g1,g2} * {g} = {(g1 * g),(g2 * g)}
thus  {g1,g2} * {g} c= {(g1 * g),(g2 * g)} :: according to XBOOLE_0:def_10 ::_thesis: {(g1 * g),(g2 * g)} c= {g1,g2} * {g}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {g1,g2} * {g} or x in {(g1 * g),(g2 * g)} )
assume  x in {g1,g2} * {g} ; ::_thesis: x in {(g1 * g),(g2 * g)}
then consider h1, h2 being Element of G such that
A1: x = h1 * h2 and
A2: h1 in {g1,g2} and
A3: h2 in {g} ;
A4: ( h1 = g1 or h1 = g2 ) by A2, TARSKI:def_2;
 h2 = g by A3, TARSKI:def_1;
hence  x in {(g1 * g),(g2 * g)} by A1, A4, TARSKI:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g1 * g),(g2 * g)} or x in {g1,g2} * {g} )
A5: g2 in {g1,g2} by TARSKI:def_2;
assume  x in {(g1 * g),(g2 * g)} ; ::_thesis: x in {g1,g2} * {g}
then A6: ( x = g1 * g or x = g2 * g ) by TARSKI:def_2;
 ( g in {g} & g1 in {g1,g2} ) by TARSKI:def_1, TARSKI:def_2;
hence  x in {g1,g2} * {g} by A6, A5; ::_thesis: verum
end;

theorem :: GROUP_2:21
for G being non empty multMagma
for g, h, g1, g2 being Element of G holds {g,h} * {g1,g2} = {(g * g1),(g * g2),(h * g1),(h * g2)}
proof
let G be non empty multMagma ; ::_thesis: for g, h, g1, g2 being Element of G holds {g,h} * {g1,g2} = {(g * g1),(g * g2),(h * g1),(h * g2)}
let g, h, g1, g2 be Element of G; ::_thesis: {g,h} * {g1,g2} = {(g * g1),(g * g2),(h * g1),(h * g2)}
set A = {g,h} * {g1,g2};
set B = {(g * g1),(g * g2),(h * g1),(h * g2)};
thus  {g,h} * {g1,g2} c= {(g * g1),(g * g2),(h * g1),(h * g2)} :: according to XBOOLE_0:def_10 ::_thesis: {(g * g1),(g * g2),(h * g1),(h * g2)} c= {g,h} * {g1,g2}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {g,h} * {g1,g2} or x in {(g * g1),(g * g2),(h * g1),(h * g2)} )
assume  x in {g,h} * {g1,g2} ; ::_thesis: x in {(g * g1),(g * g2),(h * g1),(h * g2)}
then consider h1, h2 being Element of G such that
A1: x = h1 * h2 and
A2: h1 in {g,h} and
A3: h2 in {g1,g2} ;
A4: ( h2 = g1 or h2 = g2 ) by A3, TARSKI:def_2;
 ( h1 = g or h1 = h ) by A2, TARSKI:def_2;
hence  x in {(g * g1),(g * g2),(h * g1),(h * g2)} by A1, A4, ENUMSET1:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g * g1),(g * g2),(h * g1),(h * g2)} or x in {g,h} * {g1,g2} )
A5: ( g1 in {g1,g2} & g2 in {g1,g2} ) by TARSKI:def_2;
assume  x in {(g * g1),(g * g2),(h * g1),(h * g2)} ; ::_thesis: x in {g,h} * {g1,g2}
then A6: ( x = g * g1 or x = g * g2 or x = h * g1 or x = h * g2 ) by ENUMSET1:def_2;
 ( g in {g,h} & h in {g,h} ) by TARSKI:def_2;
hence  x in {g,h} * {g1,g2} by A6, A5; ::_thesis: verum
end;

theorem Th22: :: GROUP_2:22
for G being Group
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
proof
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
proof
let x be set ; :: 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;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in 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
end;

theorem Th23: :: GROUP_2:23
for G being Group
for A being Subset of G st ( for g being Element of G st g in A holds
g " in A ) holds
A " = A
proof
let G be Group; ::_thesis: for A being Subset of G st ( for g being Element of G st g in A holds
g " in A ) holds
A " = A
let A be Subset of G; ::_thesis: ( ( for g being Element of G st g in A holds
g " in A ) implies A " = A )
assume A1: for g being Element of G st g in A holds
g " in A ; ::_thesis: A " = A
thus  A " c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= A "
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A " or x in A )
assume  x in A " ; ::_thesis: x in A
then  ex g being Element of G st
( x = g " & g in A ) ;
hence  x in A by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A " )
assume A2: x in A ; ::_thesis: x in A "
then reconsider a = x as Element of G ;
A3: x = (a ") " ;
 a " in A by A1, A2;
hence  x in A " by A3; ::_thesis: verum
end;

theorem :: GROUP_2:24
for G being non empty multMagma
for A, B being Subset of G st ( for a, b being Element of G st a in A & b in B holds
a * b = b * a ) holds
A * B = B * A
proof
let G be non empty multMagma ; ::_thesis: for A, B being Subset of G st ( for a, b being Element of G st a in A & b in B holds
a * b = b * a ) holds
A * B = B * A
let A, B be Subset of G; ::_thesis: ( ( for a, b being Element of G st a in A & b in B holds
a * b = b * a ) implies A * B = B * A )
assume A1: for a, b being Element of G st a in A & b in B holds
a * b = b * a ; ::_thesis: A * B = B * A
thus  A * B c= B * A :: according to XBOOLE_0:def_10 ::_thesis: B * A c= A * B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * B or x in B * A )
assume  x in A * B ; ::_thesis: x in B * A
then consider a, b being Element of G such that
A2: x = a * b and
A3: ( a in A & b in B ) ;
 x = b * a by A1, A2, A3;
hence  x in B * A by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B * A or x in A * B )
assume  x in B * A ; ::_thesis: x in A * B
then consider b, a being Element of G such that
A4: x = b * a and
A5: ( b in B & a in A ) ;
 x = a * b by A1, A4, A5;
hence  x in A * B by A5; ::_thesis: verum
end;

Lm2:  for A being commutative Group
for a, b being Element of A holds a * b = b * a
;

theorem Th25: :: GROUP_2:25
for G being non empty multMagma
for A, B being Subset of G st G is commutative Group holds
A * B = B * A
proof
let G be non empty multMagma ; ::_thesis: for A, B being Subset of G st G is commutative Group holds
A * B = B * A
let A, B be Subset of G; ::_thesis: ( G is commutative Group implies A * B = B * A )
assume A1: G is commutative Group ; ::_thesis: A * B = B * A
thus  A * B c= B * A :: according to XBOOLE_0:def_10 ::_thesis: B * A c= A * B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * B or x in B * A )
assume  x in A * B ; ::_thesis: x in B * A
then consider g, h being Element of G such that
A2: x = g * h and
A3: ( g in A & h in B ) ;
 x = h * g by A1, A2, Lm2;
hence  x in B * A by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B * A or x in A * B )
assume  x in B * A ; ::_thesis: x in A * B
then consider g, h being Element of G such that
A4: x = g * h and
A5: ( g in B & h in A ) ;
 x = h * g by A1, A4, Lm2;
hence  x in A * B by A5; ::_thesis: verum
end;

theorem :: GROUP_2:26
for G being commutative Group
for A, B being Subset of G holds (A * B) " = (A ") * (B ")
proof
let G be commutative Group; ::_thesis: for A, B being Subset of G holds (A * B) " = (A ") * (B ")
let A, B be Subset of G; ::_thesis: (A * B) " = (A ") * (B ")
thus  (A * B) " c= (A ") * (B ") :: according to XBOOLE_0:def_10 ::_thesis: (A ") * (B ") c= (A * B) "
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A * B) " or x in (A ") * (B ") )
assume  x in (A * B) " ; ::_thesis: x in (A ") * (B ")
then consider g being Element of G such that
A1: x = g " and
A2: g in A * B ;
consider g1, g2 being Element of G such that
A3: g = g1 * g2 and
A4: ( g1 in A & g2 in B ) by A2;
A5: ( g1 " in A " & g2 " in B " ) by A4;
 x = (g1 ") * (g2 ") by A1, A3, GROUP_1:47;
hence  x in (A ") * (B ") by A5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ") * (B ") or x in (A * B) " )
assume  x in (A ") * (B ") ; ::_thesis: x in (A * B) "
then consider g1, g2 being Element of G such that
A6: x = g1 * g2 and
A7: g1 in A " and
A8: g2 in B " ;
consider b being Element of G such that
A9: g2 = b " and
A10: b in B by A8;
consider a being Element of G such that
A11: g1 = a " and
A12: a in A by A7;
A13: a * b in A * B by A12, A10;
 x = (a * b) " by A6, A11, A9, GROUP_1:47;
hence  x in (A * B) " by A13; ::_thesis: verum
end;

definition
let G be non empty multMagma ;
let g be Element of G;
let A be Subset of G;
funcg * A ->  Subset of G equals :: GROUP_2:def 3
{g} * A;
correctness
coherence
{g} * A is Subset of G;
;
funcA * g ->  Subset of G equals :: GROUP_2:def 4
A * {g};
correctness
coherence
A * {g} is Subset of G;
;
end;

:: deftheorem  defines * GROUP_2:def_3_:_
 for G being non empty multMagma
for g being Element of G
for A being Subset of G holds g * A = {g} * A;

:: deftheorem  defines * GROUP_2:def_4_:_
 for G being non empty multMagma
for g being Element of G
for A being Subset of G holds A * g = A * {g};

theorem Th27: :: GROUP_2:27
for x being set
for G being non empty multMagma
for A being Subset of G
for g being Element of G holds
( x in g * A iff ex h being Element of G st
( x = g * h & h in A ) )
proof
let x be set ; ::_thesis: for G being non empty multMagma
for A being Subset of G
for g being Element of G holds
( x in g * A iff ex h being Element of G st
( x = g * h & h in A ) )
let G be non empty multMagma ; ::_thesis: for A being Subset of G
for g being Element of G holds
( x in g * A iff ex h being Element of G st
( x = g * h & h in A ) )
let A be Subset of G; ::_thesis: for g being Element of G holds
( x in g * A iff ex h being Element of G st
( x = g * h & h in A ) )
let g be Element of G; ::_thesis: ( x in g * A iff ex h being Element of G st
( x = g * h & h in A ) )
thus  ( x in g * A implies ex h being Element of G st
( x = g * h & h in A ) ) ::_thesis: ( ex h being Element of G st
( x = g * h & h in A ) implies x in g * A )
proof
assume  x in g * A ; ::_thesis: ex h being Element of G st
( x = g * h & h in A )
then consider g1, g2 being Element of G such that
A1: x = g1 * g2 and
A2: g1 in {g} and
A3: g2 in A ;
 g1 = g by A2, TARSKI:def_1;
hence  ex h being Element of G st
( x = g * h & h in A ) by A1, A3; ::_thesis: verum
end;
given h being Element of G such that A4: ( x = g * h & h in A ) ; ::_thesis: x in g * A
 g in {g} by TARSKI:def_1;
hence  x in g * A by A4; ::_thesis: verum
end;

theorem Th28: :: GROUP_2:28
for x being set
for G being non empty multMagma
for A being Subset of G
for g being Element of G holds
( x in A * g iff ex h being Element of G st
( x = h * g & h in A ) )
proof
let x be set ; ::_thesis: for G being non empty multMagma
for A being Subset of G
for g being Element of G holds
( x in A * g iff ex h being Element of G st
( x = h * g & h in A ) )
let G be non empty multMagma ; ::_thesis: for A being Subset of G
for g being Element of G holds
( x in A * g iff ex h being Element of G st
( x = h * g & h in A ) )
let A be Subset of G; ::_thesis: for g being Element of G holds
( x in A * g iff ex h being Element of G st
( x = h * g & h in A ) )
let g be Element of G; ::_thesis: ( x in A * g iff ex h being Element of G st
( x = h * g & h in A ) )
thus  ( x in A * g implies ex h being Element of G st
( x = h * g & h in A ) ) ::_thesis: ( ex h being Element of G st
( x = h * g & h in A ) implies x in A * g )
proof
assume  x in A * g ; ::_thesis: ex h being Element of G st
( x = h * g & h in A )
then consider g1, g2 being Element of G such that
A1: ( x = g1 * g2 & g1 in A ) and
A2: g2 in {g} ;
 g2 = g by A2, TARSKI:def_1;
hence  ex h being Element of G st
( x = h * g & h in A ) by A1; ::_thesis: verum
end;
given h being Element of G such that A3: ( x = h * g & h in A ) ; ::_thesis: x in A * g
 g in {g} by TARSKI:def_1;
hence  x in A * g by A3; ::_thesis: verum
end;

theorem :: GROUP_2:29
for G being non empty multMagma
for A, B being Subset of G
for g being Element of G st G is associative holds
(g * A) * B = g * (A * B) by Th10;

theorem :: GROUP_2:30
for G being non empty multMagma
for A, B being Subset of G
for g being Element of G st G is associative holds
(A * g) * B = A * (g * B) by Th10;

theorem :: GROUP_2:31
for G being non empty multMagma
for A, B being Subset of G
for g being Element of G st G is associative holds
(A * B) * g = A * (B * g) by Th10;

theorem Th32: :: GROUP_2:32
for G being non empty multMagma
for A being Subset of G
for g, h being Element of G st G is associative holds
(g * h) * A = g * (h * A)
proof
let G be non empty multMagma ; ::_thesis: for A being Subset of G
for g, h being Element of G st G is associative holds
(g * h) * A = g * (h * A)
let A be Subset of G; ::_thesis: for g, h being Element of G st G is associative holds
(g * h) * A = g * (h * A)
let g, h be Element of G; ::_thesis: ( G is associative implies (g * h) * A = g * (h * A) )
assume A1: G is associative ; ::_thesis: (g * h) * A = g * (h * A)
thus (g * h) * A = ({g} * {h}) * A by Th18
.= g * (h * A) by A1, Th10 ; ::_thesis: verum
end;

theorem :: GROUP_2:33
for G being non empty multMagma
for A being Subset of G
for g, h being Element of G st G is associative holds
(g * A) * h = g * (A * h) by Th10;

theorem Th34: :: GROUP_2:34
for G being non empty multMagma
for A being Subset of G
for g, h being Element of G st G is associative holds
(A * g) * h = A * (g * h)
proof
let G be non empty multMagma ; ::_thesis: for A being Subset of G
for g, h being Element of G st G is associative holds
(A * g) * h = A * (g * h)
let A be Subset of G; ::_thesis: for g, h being Element of G st G is associative holds
(A * g) * h = A * (g * h)
let g, h be Element of G; ::_thesis: ( G is associative implies (A * g) * h = A * (g * h) )
assume  G is associative ; ::_thesis: (A * g) * h = A * (g * h)
hence (A * g) * h = A * ({g} * {h}) by Th10
.= A * (g * h) by Th18 ;
::_thesis: verum
end;

theorem :: GROUP_2:35
for G being non empty multMagma
for a being Element of G holds
( ({} the carrier of G) * a = {} & a * ({} the carrier of G) = {} ) by Th16;


theorem :: GROUP_2:36
for G being Group
for a being Element of G holds
( ([#] the carrier of G) * a = the carrier of G & a * ([#] the carrier of G) = the carrier of G ) by Th17;

theorem Th37: :: GROUP_2:37
for G being non empty Group-like multMagma
for A being Subset of G holds
( (1_ G) * A = A & A * (1_ G) = A )
proof
let G be non empty Group-like multMagma ; ::_thesis: for A being Subset of G holds
( (1_ G) * A = A & A * (1_ G) = A )
let A be Subset of G; ::_thesis: ( (1_ G) * A = A & A * (1_ G) = A )
thus  (1_ G) * A = A ::_thesis: A * (1_ G) = A
proof
thus  (1_ G) * A c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= (1_ G) * A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (1_ G) * A or x in A )
assume  x in (1_ G) * A ; ::_thesis: x in A
then  ex h being Element of G st
( x = (1_ G) * h & h in A ) by Th27;
hence  x in A by GROUP_1:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in (1_ G) * A )
assume A1: x in A ; ::_thesis: x in (1_ G) * A
then reconsider a = x as Element of G ;
 (1_ G) * a = a by GROUP_1:def_4;
hence  x in (1_ G) * A by A1, Th27; ::_thesis: verum
end;
thus  A * (1_ G) c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= A * (1_ G)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * (1_ G) or x in A )
assume  x in A * (1_ G) ; ::_thesis: x in A
then  ex h being Element of G st
( x = h * (1_ G) & h in A ) by Th28;
hence  x in A by GROUP_1:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A * (1_ G) )
assume A2: x in A ; ::_thesis: x in A * (1_ G)
then reconsider a = x as Element of G ;
 a * (1_ G) = a by GROUP_1:def_4;
hence  x in A * (1_ G) by A2, Th28; ::_thesis: verum
end;

theorem :: GROUP_2:38
for G being non empty Group-like multMagma
for g being Element of G
for A being Subset of G st G is commutative Group holds
g * A = A * g by Th25;

definition
let G be non empty Group-like multMagma ;
mode Subgroup of G ->  non empty Group-like multMagma  means :Def5: :: GROUP_2:def 5
( the carrier of it c= the carrier of G & the multF of it = the multF of G || the carrier of it );
existence
 ex b1 being non empty Group-like multMagma st
( the carrier of b1 c= the carrier of G & the multF of b1 = the multF of G || the carrier of b1 )
proof
take  G ; ::_thesis: ( the carrier of G c= the carrier of G & the multF of G = the multF of G || the carrier of G )
 dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def_1;
hence  ( the carrier of G c= the carrier of G & the multF of G = the multF of G || the carrier of G ) by RELAT_1:68; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Subgroup GROUP_2:def_5_:_
 for G, b2 being non empty Group-like multMagma holds
( b2 is Subgroup of G iff ( the carrier of b2 c= the carrier of G & the multF of b2 = the multF of G || the carrier of b2 ) );


theorem Th39: :: GROUP_2:39
for G being non empty Group-like multMagma
for H being Subgroup of G st G is finite holds
H is finite
proof
let G be non empty Group-like multMagma ; ::_thesis: for H being Subgroup of G st G is finite holds
H is finite
let H be Subgroup of G; ::_thesis: ( G is finite implies H is finite )
assume A1: G is finite ; ::_thesis: H is finite
 the carrier of H c= the carrier of G by Def5;
hence  the carrier of H is finite by A1; :: according to STRUCT_0:def_11 ::_thesis: verum
end;

theorem Th40: :: GROUP_2:40
for x being set
for G being non empty Group-like multMagma
for H being Subgroup of G st x in H holds
x in G
proof
let x be set ; ::_thesis: for G being non empty Group-like multMagma
for H being Subgroup of G st x in H holds
x in G
let G be non empty Group-like multMagma ; ::_thesis: for H being Subgroup of G st x in H holds
x in G
let H be Subgroup of G; ::_thesis: ( x in H implies x in G )
assume  x in H ; ::_thesis: x in G
then A1: x in the carrier of H by STRUCT_0:def_5;
 the carrier of H c= the carrier of G by Def5;
hence  x in G by A1, STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th41: :: GROUP_2:41
for G being non empty Group-like multMagma
for H being Subgroup of G
for h being Element of H holds h in G
proof
let G be non empty Group-like multMagma ; ::_thesis: for H being Subgroup of G
for h being Element of H holds h in G
let H be Subgroup of G; ::_thesis: for h being Element of H holds h in G
let h be Element of H; ::_thesis: h in G
 h in H by STRUCT_0:def_5;
hence  h in G by Th40; ::_thesis: verum
end;

theorem Th42: :: GROUP_2:42
for G being non empty Group-like multMagma
for H being Subgroup of G
for h being Element of H holds h is Element of G
proof
let G be non empty Group-like multMagma ; ::_thesis: for H being Subgroup of G
for h being Element of H holds h is Element of G
let H be Subgroup of G; ::_thesis: for h being Element of H holds h is Element of G
let h be Element of H; ::_thesis: h is Element of G
 h in G by Th41;
hence  h is Element of G by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th43: :: GROUP_2:43
for G being non empty Group-like multMagma
for g1, g2 being Element of G
for H being Subgroup of G
for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds
h1 * h2 = g1 * g2
proof
let G be non empty Group-like multMagma ; ::_thesis: for g1, g2 being Element of G
for H being Subgroup of G
for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds
h1 * h2 = g1 * g2
let g1, g2 be Element of G; ::_thesis: for H being Subgroup of G
for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds
h1 * h2 = g1 * g2
let H be Subgroup of G; ::_thesis: for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds
h1 * h2 = g1 * g2
let h1, h2 be Element of H; ::_thesis: ( h1 = g1 & h2 = g2 implies h1 * h2 = g1 * g2 )
assume A1: ( h1 = g1 & h2 = g2 ) ; ::_thesis: h1 * h2 = g1 * g2
 h1 * h2 = ( the multF of G || the carrier of H) . [h1,h2] by Def5;
hence  h1 * h2 = g1 * g2 by A1, FUNCT_1:49; ::_thesis: verum
end;

registration
let G be Group;
cluster  ->  associative for Subgroup of G;
coherence
 for b1 being Subgroup of G holds b1 is associative
proof
let H be Subgroup of G; ::_thesis: H is associative
let x, y, z be Element of H; :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
A1: ( x in the carrier of H & y in the carrier of H ) ;
A2: ( z in the carrier of H & x * y in the carrier of H ) ;
 ( y * z in the carrier of H & the carrier of H c= the carrier of G ) by Def5;
then reconsider a = x, b = y, c = z, ab = x * y, bc = y * z as Element of G by A1, A2;
thus (x * y) * z = ab * c by Th43
.= (a * b) * c by Th43
.= a * (b * c) by GROUP_1:def_3
.= a * bc by Th43
.= x * (y * z) by Th43 ; ::_thesis: verum
end;
end;


theorem Th44: :: GROUP_2:44
for G being Group
for H being Subgroup of G holds 1_ H = 1_ G
proof
let G be Group; ::_thesis: for H being Subgroup of G holds 1_ H = 1_ G
let H be Subgroup of G; ::_thesis: 1_ H = 1_ G
set h = the Element of H;
reconsider g = the Element of H, g9 = 1_ H as Element of G by Th42;
 the Element of H * (1_ H) = the Element of H by GROUP_1:def_4;
then  g * g9 = g by Th43;
hence  1_ H = 1_ G by GROUP_1:7; ::_thesis: verum
end;

theorem :: GROUP_2:45
for G being Group
for H1, H2 being Subgroup of G holds 1_ H1 = 1_ H2
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds 1_ H1 = 1_ H2
let H1, H2 be Subgroup of G; ::_thesis: 1_ H1 = 1_ H2
thus  1_ H1 = 1_ G by Th44
.= 1_ H2 by Th44 ; ::_thesis: verum
end;

theorem Th46: :: GROUP_2:46
for G being Group
for H being Subgroup of G holds 1_ G in H
proof
let G be Group; ::_thesis: for H being Subgroup of G holds 1_ G in H
let H be Subgroup of G; ::_thesis: 1_ G in H
 1_ H in H by STRUCT_0:def_5;
hence  1_ G in H by Th44; ::_thesis: verum
end;

theorem :: GROUP_2:47
for G being Group
for H1, H2 being Subgroup of G holds 1_ H1 in H2
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds 1_ H1 in H2
let H1, H2 be Subgroup of G; ::_thesis: 1_ H1 in H2
 1_ H1 = 1_ G by Th44;
hence  1_ H1 in H2 by Th46; ::_thesis: verum
end;

theorem Th48: :: GROUP_2:48
for G being Group
for g being Element of G
for H being Subgroup of G
for h being Element of H st h = g holds
h " = g "
proof
let G be Group; ::_thesis: for g being Element of G
for H being Subgroup of G
for h being Element of H st h = g holds
h " = g "
let g be Element of G; ::_thesis: for H being Subgroup of G
for h being Element of H st h = g holds
h " = g "
let H be Subgroup of G; ::_thesis: for h being Element of H st h = g holds
h " = g "
let h be Element of H; ::_thesis: ( h = g implies h " = g " )
reconsider g9 = h " as Element of G by Th42;
A1: h * (h ") = 1_ H by GROUP_1:def_5;
assume  h = g ; ::_thesis: h " = g "
then g * g9 = 1_ H by A1, Th43
.= 1_ G by Th44 ;
hence  h " = g " by GROUP_1:12; ::_thesis: verum
end;

theorem :: GROUP_2:49
for G being Group
for H being Subgroup of G holds inverse_op H = (inverse_op G) | the carrier of H
proof
let G be Group; ::_thesis: for H being Subgroup of G holds inverse_op H = (inverse_op G) | the carrier of H
let H be Subgroup of G; ::_thesis: inverse_op H = (inverse_op G) | the carrier of H
 the carrier of H c= the carrier of G by Def5;
then A1: the carrier of G /\ the carrier of H = the carrier of H by XBOOLE_1:28;
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(inverse_op_H)_holds_
(inverse_op_H)_._x_=_(inverse_op_G)_._x
let x be set ; ::_thesis: ( x in dom (inverse_op H) implies (inverse_op H) . x = (inverse_op G) . x )
assume  x in dom (inverse_op H) ; ::_thesis: (inverse_op H) . x = (inverse_op G) . x
then reconsider a = x as Element of H ;
reconsider b = a as Element of G by Th42;
thus (inverse_op H) . x = a " by GROUP_1:def_6
.= b " by Th48
.= (inverse_op G) . x by GROUP_1:def_6 ; ::_thesis: verum
end;
 ( dom (inverse_op H) = the carrier of H & dom (inverse_op G) = the carrier of G ) by FUNCT_2:def_1;
hence  inverse_op H = (inverse_op G) | the carrier of H by A1, A2, FUNCT_1:46; ::_thesis: verum
end;

theorem Th50: :: GROUP_2:50
for G being Group
for g1, g2 being Element of G
for H being Subgroup of G st g1 in H & g2 in H holds
g1 * g2 in H
proof
let G be Group; ::_thesis: for g1, g2 being Element of G
for H being Subgroup of G st g1 in H & g2 in H holds
g1 * g2 in H
let g1, g2 be Element of G; ::_thesis: for H being Subgroup of G st g1 in H & g2 in H holds
g1 * g2 in H
let H be Subgroup of G; ::_thesis: ( g1 in H & g2 in H implies g1 * g2 in H )
assume  ( g1 in H & g2 in H ) ; ::_thesis: g1 * g2 in H
then reconsider h1 = g1, h2 = g2 as Element of H by STRUCT_0:def_5;
 h1 * h2 in H by STRUCT_0:def_5;
hence  g1 * g2 in H by Th43; ::_thesis: verum
end;

theorem Th51: :: GROUP_2:51
for G being Group
for g being Element of G
for H being Subgroup of G st g in H holds
g " in H
proof
let G be Group; ::_thesis: for g being Element of G
for H being Subgroup of G st g in H holds
g " in H
let g be Element of G; ::_thesis: for H being Subgroup of G st g in H holds
g " in H
let H be Subgroup of G; ::_thesis: ( g in H implies g " in H )
assume  g in H ; ::_thesis: g " in H
then reconsider h = g as Element of H by STRUCT_0:def_5;
 h " in H by STRUCT_0:def_5;
hence  g " in H by Th48; ::_thesis: verum
end;

registration
let G be Group;
cluster non empty strict unital Group-like associative for Subgroup of G;
existence
 ex b1 being Subgroup of G st b1 is strict
proof
set H = multMagma(# the carrier of G, the multF of G #);
 multMagma(# the carrier of G, the multF of G #) is Group-like
proof
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 b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) holds
( b1 * t = b1 & t * b1 = b1 & ex b2 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( b1 * b2 = t & b2 * b1 = t ) )
let a be Element of multMagma(# the carrier of G, the multF of G #); ::_thesis: ( a * t = a & t * a = a & ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( a * b1 = t & b1 * 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 b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( a * b1 = t & b1 * a = t ) )
thus t * a = (1_ G) * x
.= a by GROUP_1:def_4 ; ::_thesis: ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( a * b1 = t & b1 * 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;
then reconsider H = multMagma(# the carrier of G, the multF of G #) as non empty Group-like multMagma ;
 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 b1 being Subgroup of G st b1 is strict ; ::_thesis: verum
end;
end;

theorem Th52: :: GROUP_2:52
for G being Group
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
proof
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__::_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 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 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
end;

theorem Th53: :: GROUP_2:53
for G being Group
for H being Subgroup of G st G is commutative Group holds
H is commutative
proof
let G be Group; ::_thesis: for H being Subgroup of G st G is commutative Group holds
H is commutative
let H be Subgroup of G; ::_thesis: ( G is commutative Group implies H is commutative )
assume A1: G is commutative Group ; ::_thesis: H is commutative
thus  for h1, h2 being Element of H holds h1 * h2 = h2 * h1 :: according to GROUP_1:def_12 ::_thesis: verum
proof
let h1, h2 be Element of H; ::_thesis: h1 * h2 = h2 * h1
reconsider g1 = h1, g2 = h2 as Element of G by Th42;
thus h1 * h2 = g1 * g2 by Th43
.= g2 * g1 by A1, Lm2
.= h2 * h1 by Th43 ; ::_thesis: verum
end;
end;

registration
let G be commutative Group;
cluster  ->  commutative for Subgroup of G;
coherence
 for b1 being Subgroup of G holds b1 is commutative by Th53;
end;

theorem Th54: :: GROUP_2:54
for G being Group holds G is Subgroup of G
proof
let G be Group; ::_thesis: G is Subgroup of G
 dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def_1;
hence  ( the carrier of G c= the carrier of G & the multF of G = the multF of G || the carrier of G ) by RELAT_1:68; :: according to GROUP_2:def_5 ::_thesis: verum
end;

theorem Th55: :: GROUP_2:55
for G1, G2 being Group st G1 is Subgroup of G2 & G2 is Subgroup of G1 holds
multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #)
proof
let G1, G2 be Group; ::_thesis: ( G1 is Subgroup of G2 & G2 is Subgroup of G1 implies multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) )
assume that
A1: G1 is Subgroup of G2 and
A2: G2 is Subgroup of G1 ; ::_thesis: multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #)
set g = the multF of G2;
set f = the multF of G1;
set B = the carrier of G2;
set A = the carrier of G1;
A3: ( the carrier of G1 c= the carrier of G2 & the carrier of G2 c= the carrier of G1 ) by A1, A2, Def5;
then A4: the carrier of G1 = the carrier of G2 by XBOOLE_0:def_10;
the multF of G1 = the multF of G2 || the carrier of G1 by A1, Def5
.= ( the multF of G1 || the carrier of G2) || the carrier of G1 by A2, Def5
.= the multF of G1 || the carrier of G2 by A4, RELAT_1:72
.= the multF of G2 by A2, Def5 ;
hence  multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th56: :: GROUP_2:56
for G1, G2, G3 being Group st G1 is Subgroup of G2 & G2 is Subgroup of G3 holds
G1 is Subgroup of G3
proof
let G1, G2, G3 be Group; ::_thesis: ( G1 is Subgroup of G2 & G2 is Subgroup of G3 implies G1 is Subgroup of G3 )
assume that
A1: G1 is Subgroup of G2 and
A2: G2 is Subgroup of G3 ; ::_thesis: G1 is Subgroup of G3
set h = the multF of G3;
set C = the carrier of G3;
set B = the carrier of G2;
set A = the carrier of G1;
A3: the carrier of G1 c= the carrier of G2 by A1, Def5;
then A4: [: the carrier of G1, the carrier of G1:] c= [: the carrier of G2, the carrier of G2:] by ZFMISC_1:96;
 the carrier of G2 c= the carrier of G3 by A2, Def5;
then A5: the carrier of G1 c= the carrier of G3 by A3, XBOOLE_1:1;
the multF of G1 = the multF of G2 || the carrier of G1 by A1, Def5
.= ( the multF of G3 || the carrier of G2) || the carrier of G1 by A2, Def5
.= the multF of G3 || the carrier of G1 by A4, FUNCT_1:51 ;
hence  G1 is Subgroup of G3 by A5, Def5; ::_thesis: verum
end;

theorem Th57: :: GROUP_2:57
for G being Group
for H1, H2 being Subgroup of G st the carrier of H1 c= the carrier of H2 holds
H1 is Subgroup of H2
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G st the carrier of H1 c= the carrier of H2 holds
H1 is Subgroup of H2
let H1, H2 be Subgroup of G; ::_thesis: ( the carrier of H1 c= the carrier of H2 implies H1 is Subgroup of H2 )
set A = the carrier of H1;
set B = the carrier of H2;
set h = the multF of G;
assume A1: the carrier of H1 c= the carrier of H2 ; ::_thesis: H1 is Subgroup of H2
hence  the carrier of H1 c= the carrier of H2 ; :: according to GROUP_2:def_5 ::_thesis: the multF of H1 = the multF of H2 || the carrier of H1
A2: [: the carrier of H1, the carrier of H1:] c= [: the carrier of H2, the carrier of H2:] by A1, ZFMISC_1:96;
 ( the multF of H1 = the multF of G || the carrier of H1 & the multF of H2 = the multF of G || the carrier of H2 ) by Def5;
hence  the multF of H1 = the multF of H2 || the carrier of H1 by A2, FUNCT_1:51; ::_thesis: verum
end;

theorem Th58: :: GROUP_2:58
for G being Group
for H1, H2 being Subgroup of G st ( for g being Element of G st g in H1 holds
g in H2 ) holds
H1 is Subgroup of H2
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G st ( for g being Element of G st g in H1 holds
g in H2 ) holds
H1 is Subgroup of H2
let H1, H2 be Subgroup of G; ::_thesis: ( ( for g being Element of G st g in H1 holds
g in H2 ) implies H1 is Subgroup of H2 )
assume A1: for g being Element of G st g in H1 holds
g in H2 ; ::_thesis: H1 is Subgroup of H2
 the carrier of H1 c= the carrier of H2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of H1 or x in the carrier of H2 )
assume  x in the carrier of H1 ; ::_thesis: x in the carrier of H2
then reconsider g = x as Element of H1 ;
reconsider g = g as Element of G by Th42;
 g in H1 by STRUCT_0:def_5;
then  g in H2 by A1;
hence  x in the carrier of H2 by STRUCT_0:def_5; ::_thesis: verum
end;
hence  H1 is Subgroup of H2 by Th57; ::_thesis: verum
end;

theorem Th59: :: GROUP_2:59
for G being Group
for H1, H2 being Subgroup of G st the carrier of H1 = the carrier of H2 holds
multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G st the carrier of H1 = the carrier of H2 holds
multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)
let H1, H2 be Subgroup of G; ::_thesis: ( the carrier of H1 = the carrier of H2 implies multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) )
assume  the carrier of H1 = the carrier of H2 ; ::_thesis: multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)
then  ( H1 is Subgroup of H2 & H2 is Subgroup of H1 ) by Th57;
hence  multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) by Th55; ::_thesis: verum
end;

theorem Th60: :: GROUP_2:60
for G being Group
for H1, H2 being Subgroup of G st ( for g being Element of G holds
( g in H1 iff g in H2 ) ) holds
multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G st ( for g being Element of G holds
( g in H1 iff g in H2 ) ) holds
multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)
let H1, H2 be Subgroup of G; ::_thesis: ( ( for g being Element of G holds
( g in H1 iff g in H2 ) ) implies multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) )
assume  for g being Element of G holds
( g in H1 iff g in H2 ) ; ::_thesis: multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)
then  ( H1 is Subgroup of H2 & H2 is Subgroup of H1 ) by Th58;
hence  multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) by Th55; ::_thesis: verum
end;

definition
let G be Group;
let H1, H2 be strict Subgroup of G;
:: original: =
redefine predH1 = H2 means :: GROUP_2:def 6
 for g being Element of G holds
( g in H1 iff g in H2 );
compatibility
 ( H1 = H2 iff for g being Element of G holds
( g in H1 iff g in H2 ) ) by Th60;
end;

:: deftheorem  defines = GROUP_2:def_6_:_
 for G being Group
for H1, H2 being strict Subgroup of G holds
( H1 = H2 iff for g being Element of G holds
( g in H1 iff g in H2 ) );

theorem Th61: :: GROUP_2:61
for G being Group
for H being Subgroup of G st the carrier of G c= the carrier of H holds
multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)
proof
let G be Group; ::_thesis: for H being Subgroup of G st the carrier of G c= the carrier of H holds
multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)
let H be Subgroup of G; ::_thesis: ( the carrier of G c= the carrier of H implies multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) )
assume A1: the carrier of G c= the carrier of H ; ::_thesis: multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)
A2: G is Subgroup of G by Th54;
 the carrier of H c= the carrier of G by Def5;
then  the carrier of G = the carrier of H by A1, XBOOLE_0:def_10;
hence  multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) by A2, Th59; ::_thesis: verum
end;

theorem Th62: :: GROUP_2:62
for G being Group
for H being Subgroup of G st ( for g being Element of G holds g in H ) holds
multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)
proof
let G be Group; ::_thesis: for H being Subgroup of G st ( for g being Element of G holds g in H ) holds
multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)
let H be Subgroup of G; ::_thesis: ( ( for g being Element of G holds g in H ) implies multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) )
assume  for g being Element of G holds g in H ; ::_thesis: multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)
then A1: for g being Element of G holds
( ( g in H implies g in G ) & ( g in G implies g in H ) ) by STRUCT_0:def_5;
 G is Subgroup of G by Th54;
hence  multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) by A1, Th60; ::_thesis: verum
end;

definition
let G be Group;
func (1). G ->  strict Subgroup of G means :Def7: :: GROUP_2:def 7
 the carrier of it = {(1_ G)};
existence
 ex b1 being strict Subgroup of G st the carrier of b1 = {(1_ G)}
proof
A1: now__::_thesis:_for_g_being_Element_of_G_st_g_in_{(1__G)}_holds_
g_"_in_{(1__G)}
let g be Element of G; ::_thesis: ( g in {(1_ G)} implies g " in {(1_ G)} )
assume  g in {(1_ G)} ; ::_thesis: g " in {(1_ G)}
then  g = 1_ G by TARSKI:def_1;
then  g " = 1_ G by GROUP_1:8;
hence  g " in {(1_ G)} by TARSKI:def_1; ::_thesis: verum
end;
now__::_thesis:_for_g1,_g2_being_Element_of_G_st_g1_in_{(1__G)}_&_g2_in_{(1__G)}_holds_
g1_*_g2_in_{(1__G)}
let g1, g2 be Element of G; ::_thesis: ( g1 in {(1_ G)} & g2 in {(1_ G)} implies g1 * g2 in {(1_ G)} )
assume  ( g1 in {(1_ G)} & g2 in {(1_ G)} ) ; ::_thesis: g1 * g2 in {(1_ G)}
then  ( g1 = 1_ G & g2 = 1_ G ) by TARSKI:def_1;
then  g1 * g2 = 1_ G by GROUP_1:def_4;
hence  g1 * g2 in {(1_ G)} by TARSKI:def_1; ::_thesis: verum
end;
hence  ex b1 being strict Subgroup of G st the carrier of b1 = {(1_ G)} by A1, Th52; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Subgroup of G st the carrier of b1 = {(1_ G)} & the carrier of b2 = {(1_ G)} holds
b1 = b2 by Th59;
end;

:: deftheorem Def7 defines (1). GROUP_2:def_7_:_
 for G being Group
for b2 being strict Subgroup of G holds
( b2 = (1). G iff the carrier of b2 = {(1_ G)} );

definition
let G be Group;
func (Omega). G ->  strict Subgroup of G equals :: GROUP_2:def 8
 multMagma(# the carrier of G, the multF of G #);
coherence
 multMagma(# the carrier of G, the multF of G #) is strict Subgroup of G
proof
set H = multMagma(# the carrier of G, the multF of G #);
 multMagma(# the carrier of G, the multF of G #) is Group-like
proof
consider e9 being Element of G such that
A1: for h being Element of G holds
( h * e9 = h & e9 * h = h & ex g being Element of G st
( h * g = e9 & g * h = e9 ) ) by GROUP_1:def_2;
reconsider e = e9 as Element of multMagma(# the carrier of G, the multF of G #) ;
take  e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of multMagma(# the carrier of G, the multF of G #); ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( h * b1 = e & b1 * h = e ) )
reconsider h9 = h as Element of G ;
consider g9 being Element of G such that
A2: ( h9 * g9 = e9 & g9 * h9 = e9 ) by A1;
 ( h9 * e9 = h9 & e9 * h9 = h9 ) by A1;
hence  ( h * e = h & e * h = h ) ; ::_thesis: ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( h * b1 = e & b1 * h = e )
reconsider g = g9 as Element of multMagma(# the carrier of G, the multF of G #) ;
take  g ; ::_thesis: ( h * g = e & g * h = e )
thus  ( h * g = e & g * h = e ) by A2; ::_thesis: verum
end;
then reconsider H = multMagma(# the carrier of G, the multF of G #) as non empty Group-like multMagma ;
 dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def_1;
then  the multF of H = the multF of G || the carrier of H by RELAT_1:68;
hence  multMagma(# the carrier of G, the multF of G #) is strict Subgroup of G by Def5; ::_thesis: verum
end;
projectivity
 for b1 being strict Subgroup of G
for b2 being Group st b1 = multMagma(# the carrier of b2, the multF of b2 #) holds
b1 = multMagma(# the carrier of b1, the multF of b1 #) ;
end;

:: deftheorem  defines (Omega). GROUP_2:def_8_:_
 for G being Group holds (Omega). G = multMagma(# the carrier of G, the multF of G #);

theorem Th63: :: GROUP_2:63
for G being Group
for H being Subgroup of G holds (1). H = (1). G
proof
let G be Group; ::_thesis: for H being Subgroup of G holds (1). H = (1). G
let H be Subgroup of G; ::_thesis: (1). H = (1). G
A1: 1_ H = 1_ G by Th44;
 ( (1). H is Subgroup of G & the carrier of ((1). H) = {(1_ H)} ) by Def7, Th56;
hence  (1). H = (1). G by A1, Def7; ::_thesis: verum
end;

theorem :: GROUP_2:64
for G being Group
for H1, H2 being Subgroup of G holds (1). H1 = (1). H2
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds (1). H1 = (1). H2
let H1, H2 be Subgroup of G; ::_thesis: (1). H1 = (1). H2
thus  (1). H1 = (1). G by Th63
.= (1). H2 by Th63 ; ::_thesis: verum
end;

theorem Th65: :: GROUP_2:65
for G being Group
for H being Subgroup of G holds (1). G is Subgroup of H
proof
let G be Group; ::_thesis: for H being Subgroup of G holds (1). G is Subgroup of H
let H be Subgroup of G; ::_thesis: (1). G is Subgroup of H
 (1). G = (1). H by Th63;
hence  (1). G is Subgroup of H ; ::_thesis: verum
end;

theorem :: GROUP_2:66
for G being strict Group
for H being Subgroup of G holds H is Subgroup of (Omega). G ;

theorem :: GROUP_2:67
for G being strict Group holds G is Subgroup of (Omega). G ;

theorem Th68: :: GROUP_2:68
for G being Group holds (1). G is finite
proof
let G be Group; ::_thesis: (1). G is finite
 the carrier of ((1). G) = {(1_ G)} by Def7;
hence  (1). G is finite ; ::_thesis: verum
end;

registration
let G be Group;
cluster (1). G ->  finite strict ;
coherence
 (1). G is finite by Th68;
cluster non empty finite strict unital Group-like associative for Subgroup of G;
existence
 ex b1 being Subgroup of G st
( b1 is strict & b1 is finite )
proof
take  (1). G ; ::_thesis: ( (1). G is strict & (1). G is finite )
thus  ( (1). G is strict & (1). G is finite ) ; ::_thesis: verum
end;
end;

registration
cluster non empty finite strict unital Group-like associative for multMagma ;
existence
 ex b1 being Group st
( b1 is strict & b1 is finite )
proof
set G = the Group;
take  (1). the Group ; ::_thesis: ( (1). the Group is strict & (1). the Group is finite )
thus  ( (1). the Group is strict & (1). the Group is finite ) ; ::_thesis: verum
end;
end;

registration
let G be finite Group;
cluster  ->  finite for Subgroup of G;
coherence
 for b1 being Subgroup of G holds b1 is finite by Th39;
end;

theorem Th69: :: GROUP_2:69
for G being Group holds card ((1). G) = 1
proof
let G be Group; ::_thesis: card ((1). G) = 1
 the carrier of ((1). G) = {(1_ G)} by Def7;
hence  card ((1). G) = 1 by CARD_1:30; ::_thesis: verum
end;

theorem Th70: :: GROUP_2:70
for G being Group
for H being finite strict Subgroup of G st card H = 1 holds
H = (1). G
proof
let G be Group; ::_thesis: for H being finite strict Subgroup of G st card H = 1 holds
H = (1). G
let H be finite strict Subgroup of G; ::_thesis: ( card H = 1 implies H = (1). G )
assume  card H = 1 ; ::_thesis: H = (1). G
then consider x being set  such that
A1: the carrier of H = {x} by CARD_2:42;
 1_ G in H by Th46;
then  1_ G in the carrier of H by STRUCT_0:def_5;
then  x = 1_ G by A1, TARSKI:def_1;
hence  H = (1). G by A1, Def7; ::_thesis: verum
end;

theorem :: GROUP_2:71
for G being Group
for H being Subgroup of G holds card H c= card G
proof
let G be Group; ::_thesis: for H being Subgroup of G holds card H c= card G
let H be Subgroup of G; ::_thesis: card H c= card G
 the carrier of H c= the carrier of G by Def5;
hence  card H c= card G by CARD_1:11; ::_thesis: verum
end;

theorem :: GROUP_2:72
for G being finite Group
for H being Subgroup of G holds card H <= card G
proof
let G be finite Group; ::_thesis: for H being Subgroup of G holds card H <= card G
let H be Subgroup of G; ::_thesis: card H <= card G
 the carrier of H c= the carrier of G by Def5;
hence  card H <= card G by NAT_1:43; ::_thesis: verum
end;

theorem :: GROUP_2:73
for G being finite Group
for H being Subgroup of G st card G = card H holds
multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)
proof
let G be finite Group; ::_thesis: for H being Subgroup of G st card G = card H holds
multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)
let H be Subgroup of G; ::_thesis: ( card G = card H implies multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) )
assume A1: card G = card H ; ::_thesis: multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #)
A2: the carrier of H c= the carrier of G by Def5;
 the carrier of H = the carrier of G
proof
assume  the carrier of H <> the carrier of G ; ::_thesis: contradiction
then  the carrier of H c< the carrier of G by A2, XBOOLE_0:def_8;
hence  contradiction by A1, CARD_2:48; ::_thesis: verum
end;
hence  multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) by Th61; ::_thesis: verum
end;

definition
let G be Group;
let H be Subgroup of G;
func carr H ->  Subset of G equals :: GROUP_2:def 9
 the carrier of H;
coherence
 the carrier of H is Subset of G by Def5;
end;

:: deftheorem  defines carr GROUP_2:def_9_:_
 for G being Group
for H being Subgroup of G holds carr H = the carrier of H;

theorem Th74: :: GROUP_2:74
for G being Group
for g1, g2 being Element of G
for H being Subgroup of G st g1 in carr H & g2 in carr H holds
g1 * g2 in carr H
proof
let G be Group; ::_thesis: for g1, g2 being Element of G
for H being Subgroup of G st g1 in carr H & g2 in carr H holds
g1 * g2 in carr H
let g1, g2 be Element of G; ::_thesis: for H being Subgroup of G st g1 in carr H & g2 in carr H holds
g1 * g2 in carr H
let H be Subgroup of G; ::_thesis: ( g1 in carr H & g2 in carr H implies g1 * g2 in carr H )
assume  ( g1 in carr H & g2 in carr H ) ; ::_thesis: g1 * g2 in carr H
then  ( g1 in H & g2 in H ) by STRUCT_0:def_5;
then  g1 * g2 in H by Th50;
hence  g1 * g2 in carr H by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th75: :: GROUP_2:75
for G being Group
for g being Element of G
for H being Subgroup of G st g in carr H holds
g " in carr H
proof
let G be Group; ::_thesis: for g being Element of G
for H being Subgroup of G st g in carr H holds
g " in carr H
let g be Element of G; ::_thesis: for H being Subgroup of G st g in carr H holds
g " in carr H
let H be Subgroup of G; ::_thesis: ( g in carr H implies g " in carr H )
assume  g in carr H ; ::_thesis: g " in carr H
then  g in H by STRUCT_0:def_5;
then  g " in H by Th51;
hence  g " in carr H by STRUCT_0:def_5; ::_thesis: verum
end;

theorem :: GROUP_2:76
for G being Group
for H being Subgroup of G holds (carr H) * (carr H) = carr H
proof
let G be Group; ::_thesis: for H being Subgroup of G holds (carr H) * (carr H) = carr H
let H be Subgroup of G; ::_thesis: (carr H) * (carr H) = carr H
A1: for g being Element of G st g in carr H holds
g " in carr H by Th75;
 for g1, g2 being Element of G st g1 in carr H & g2 in carr H holds
g1 * g2 in carr H by Th74;
hence  (carr H) * (carr H) = carr H by A1, Th22; ::_thesis: verum
end;

theorem :: GROUP_2:77
for G being Group
for H being Subgroup of G holds (carr H) " = carr H
proof
let G be Group; ::_thesis: for H being Subgroup of G holds (carr H) " = carr H
let H be Subgroup of G; ::_thesis: (carr H) " = carr H
 for g being Element of G st g in carr H holds
g " in carr H by Th75;
hence  (carr H) " = carr H by Th23; ::_thesis: verum
end;

theorem Th78: :: GROUP_2:78
for G being Group
for H1, H2 being Subgroup of G holds
( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) )
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds
( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) )
let H1, H2 be Subgroup of G; ::_thesis: ( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) )
thus  ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) ::_thesis: ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) )
proof
assume A1: (carr H1) * (carr H2) = (carr H2) * (carr H1) ; ::_thesis: ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2)
A2: now__::_thesis:_for_g_being_Element_of_G_st_g_in_(carr_H1)_*_(carr_H2)_holds_
g_"_in_(carr_H1)_*_(carr_H2)
let g be Element of G; ::_thesis: ( g in (carr H1) * (carr H2) implies g " in (carr H1) * (carr H2) )
assume A3: g in (carr H1) * (carr H2) ; ::_thesis: g " in (carr H1) * (carr H2)
then consider a, b being Element of G such that
A4: g = a * b and
 a in carr H1 and
 b in carr H2 ;
consider b1, a1 being Element of G such that
A5: a * b = b1 * a1 and
A6: ( b1 in carr H2 & a1 in carr H1 ) by A1, A3, A4;
A7: ( a1 " in carr H1 & b1 " in carr H2 ) by A6, Th75;
 g " = (a1 ") * (b1 ") by A4, A5, GROUP_1:17;
hence  g " in (carr H1) * (carr H2) by A7; ::_thesis: verum
end;
A8: now__::_thesis:_for_g1,_g2_being_Element_of_G_st_g1_in_(carr_H1)_*_(carr_H2)_&_g2_in_(carr_H1)_*_(carr_H2)_holds_
g1_*_g2_in_(carr_H1)_*_(carr_H2)
let g1, g2 be Element of G; ::_thesis: ( g1 in (carr H1) * (carr H2) & g2 in (carr H1) * (carr H2) implies g1 * g2 in (carr H1) * (carr H2) )
assume that
A9: g1 in (carr H1) * (carr H2) and
A10: g2 in (carr H1) * (carr H2) ; ::_thesis: g1 * g2 in (carr H1) * (carr H2)
consider a1, b1 being Element of G such that
A11: g1 = a1 * b1 and
A12: a1 in carr H1 and
A13: b1 in carr H2 by A9;
consider a2, b2 being Element of G such that
A14: g2 = a2 * b2 and
A15: a2 in carr H1 and
A16: b2 in carr H2 by A10;
 b1 * a2 in (carr H1) * (carr H2) by A1, A13, A15;
then consider a, b being Element of G such that
A17: b1 * a2 = a * b and
A18: a in carr H1 and
A19: b in carr H2 ;
A20: b * b2 in carr H2 by A16, A19, Th74;
g1 * g2 = ((a1 * b1) * a2) * b2 by A11, A14, GROUP_1:def_3
.= (a1 * (b1 * a2)) * b2 by GROUP_1:def_3 ;
then A21: g1 * g2 = ((a1 * a) * b) * b2 by A17, GROUP_1:def_3
.= (a1 * a) * (b * b2) by GROUP_1:def_3 ;
 a1 * a in carr H1 by A12, A18, Th74;
hence  g1 * g2 in (carr H1) * (carr H2) by A21, A20; ::_thesis: verum
end;
 (carr H1) * (carr H2) <> {} by Th9;
hence  ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) by A8, A2, Th52; ::_thesis: verum
end;
given H being Subgroup of G such that A22: the carrier of H = (carr H1) * (carr H2) ; ::_thesis: (carr H1) * (carr H2) = (carr H2) * (carr H1)
thus  (carr H1) * (carr H2) c= (carr H2) * (carr H1) :: according to XBOOLE_0:def_10 ::_thesis: (carr H2) * (carr H1) c= (carr H1) * (carr H2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (carr H1) * (carr H2) or x in (carr H2) * (carr H1) )
assume A23: x in (carr H1) * (carr H2) ; ::_thesis: x in (carr H2) * (carr H1)
then reconsider y = x as Element of G ;
 y " in carr H by A22, A23, Th75;
then consider a, b being Element of G such that
A24: y " = a * b and
A25: ( a in carr H1 & b in carr H2 ) by A22;
A26: y = (y ") "
.= (b ") * (a ") by A24, GROUP_1:17 ;
 ( a " in carr H1 & b " in carr H2 ) by A25, Th75;
hence  x in (carr H2) * (carr H1) by A26; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (carr H2) * (carr H1) or x in (carr H1) * (carr H2) )
assume A27: x in (carr H2) * (carr H1) ; ::_thesis: x in (carr H1) * (carr H2)
then reconsider y = x as Element of G ;
consider a, b being Element of G such that
A28: ( x = a * b & a in carr H2 ) and
A29: b in carr H1 by A27;
now__::_thesis:_y_"_in_carr_H
A30: b " in carr H1 by A29, Th75;
assume A31: not y " in carr H ; ::_thesis: contradiction
 ( y " = (b ") * (a ") & a " in carr H2 ) by A28, Th75, GROUP_1:17;
hence  contradiction by A22, A31, A30; ::_thesis: verum
end;
then  (y ") " in carr H by Th75;
hence  x in (carr H1) * (carr H2) by A22; ::_thesis: verum
end;

theorem :: GROUP_2:79
for G being Group
for H1, H2 being Subgroup of G st G is commutative Group holds
ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2)
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G st G is commutative Group holds
ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2)
let H1, H2 be Subgroup of G; ::_thesis: ( G is commutative Group implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) )
assume  G is commutative Group ; ::_thesis: ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2)
then  (carr H1) * (carr H2) = (carr H2) * (carr H1) by Th25;
hence  ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) by Th78; ::_thesis: verum
end;

definition
let G be Group;
let H1, H2 be Subgroup of G;
funcH1 /\ H2 ->  strict Subgroup of G means :Def10: :: GROUP_2:def 10
 the carrier of it = (carr H1) /\ (carr H2);
existence
 ex b1 being strict Subgroup of G st the carrier of b1 = (carr H1) /\ (carr H2)
proof
set A = (carr H1) /\ (carr H2);
 1_ G in H2 by Th46;
then A1: 1_ G in the carrier of H2 by STRUCT_0:def_5;
A2: now__::_thesis:_for_g1,_g2_being_Element_of_G_st_g1_in_(carr_H1)_/\_(carr_H2)_&_g2_in_(carr_H1)_/\_(carr_H2)_holds_
g1_*_g2_in_(carr_H1)_/\_(carr_H2)
let g1, g2 be Element of G; ::_thesis: ( g1 in (carr H1) /\ (carr H2) & g2 in (carr H1) /\ (carr H2) implies g1 * g2 in (carr H1) /\ (carr H2) )
assume A3: ( g1 in (carr H1) /\ (carr H2) & g2 in (carr H1) /\ (carr H2) ) ; ::_thesis: g1 * g2 in (carr H1) /\ (carr H2)
then  ( g1 in carr H2 & g2 in carr H2 ) by XBOOLE_0:def_4;
then A4: g1 * g2 in carr H2 by Th74;
 ( g1 in carr H1 & g2 in carr H1 ) by A3, XBOOLE_0:def_4;
then  g1 * g2 in carr H1 by Th74;
hence  g1 * g2 in (carr H1) /\ (carr H2) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
A5: now__::_thesis:_for_g_being_Element_of_G_st_g_in_(carr_H1)_/\_(carr_H2)_holds_
g_"_in_(carr_H1)_/\_(carr_H2)
let g be Element of G; ::_thesis: ( g in (carr H1) /\ (carr H2) implies g " in (carr H1) /\ (carr H2) )
assume A6: g in (carr H1) /\ (carr H2) ; ::_thesis: g " in (carr H1) /\ (carr H2)
then  g in carr H2 by XBOOLE_0:def_4;
then A7: g " in carr H2 by Th75;
 g in carr H1 by A6, XBOOLE_0:def_4;
then  g " in carr H1 by Th75;
hence  g " in (carr H1) /\ (carr H2) by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
 1_ G in H1 by Th46;
then  1_ G in the carrier of H1 by STRUCT_0:def_5;
then  (carr H1) /\ (carr H2) <> {} by A1, XBOOLE_0:def_4;
hence  ex b1 being strict Subgroup of G st the carrier of b1 = (carr H1) /\ (carr H2) by A2, A5, Th52; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Subgroup of G st the carrier of b1 = (carr H1) /\ (carr H2) & the carrier of b2 = (carr H1) /\ (carr H2) holds
b1 = b2 by Th59;
end;

:: deftheorem Def10 defines /\ GROUP_2:def_10_:_
 for G being Group
for H1, H2 being Subgroup of G
for b4 being strict Subgroup of G holds
( b4 = H1 /\ H2 iff the carrier of b4 = (carr H1) /\ (carr H2) );

theorem Th80: :: GROUP_2:80
for G being Group
for H1, H2 being Subgroup of G holds
( ( for H being Subgroup of G st H = H1 /\ H2 holds
the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds
H = H1 /\ H2 ) )
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds
( ( for H being Subgroup of G st H = H1 /\ H2 holds
the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds
H = H1 /\ H2 ) )
let H1, H2 be Subgroup of G; ::_thesis: ( ( for H being Subgroup of G st H = H1 /\ H2 holds
the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds
H = H1 /\ H2 ) )
A1: ( the carrier of H1 = carr H1 & the carrier of H2 = carr H2 ) ;
thus  for H being Subgroup of G st H = H1 /\ H2 holds
the carrier of H = the carrier of H1 /\ the carrier of H2 ::_thesis: for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds
H = H1 /\ H2
proof
let H be Subgroup of G; ::_thesis: ( H = H1 /\ H2 implies the carrier of H = the carrier of H1 /\ the carrier of H2 )
assume  H = H1 /\ H2 ; ::_thesis: the carrier of H = the carrier of H1 /\ the carrier of H2
hence  the carrier of H = (carr H1) /\ (carr H2) by Def10
.= the carrier of H1 /\ the carrier of H2 ;
::_thesis: verum
end;
let H be strict Subgroup of G; ::_thesis: ( the carrier of H = the carrier of H1 /\ the carrier of H2 implies H = H1 /\ H2 )
assume  the carrier of H = the carrier of H1 /\ the carrier of H2 ; ::_thesis: H = H1 /\ H2
hence  H = H1 /\ H2 by A1, Def10; ::_thesis: verum
end;

theorem :: GROUP_2:81
for G being Group
for H1, H2 being Subgroup of G holds carr (H1 /\ H2) = (carr H1) /\ (carr H2) by Def10;

theorem Th82: :: GROUP_2:82
for x being set
for G being Group
for H1, H2 being Subgroup of G holds
( x in H1 /\ H2 iff ( x in H1 & x in H2 ) )
proof
let x be set ; ::_thesis: for G being Group
for H1, H2 being Subgroup of G holds
( x in H1 /\ H2 iff ( x in H1 & x in H2 ) )
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds
( x in H1 /\ H2 iff ( x in H1 & x in H2 ) )
let H1, H2 be Subgroup of G; ::_thesis: ( x in H1 /\ H2 iff ( x in H1 & x in H2 ) )
thus  ( x in H1 /\ H2 implies ( x in H1 & x in H2 ) ) ::_thesis: ( x in H1 & x in H2 implies x in H1 /\ H2 )
proof
assume  x in H1 /\ H2 ; ::_thesis: ( x in H1 & x in H2 )
then  x in the carrier of (H1 /\ H2) by STRUCT_0:def_5;
then  x in (carr H1) /\ (carr H2) by Def10;
then  ( x in carr H1 & x in carr H2 ) by XBOOLE_0:def_4;
hence  ( x in H1 & x in H2 ) by STRUCT_0:def_5; ::_thesis: verum
end;
assume  ( x in H1 & x in H2 ) ; ::_thesis: x in H1 /\ H2
then  ( x in carr H2 & x in carr H1 ) by STRUCT_0:def_5;
then  x in (carr H1) /\ (carr H2) by XBOOLE_0:def_4;
then  x in carr (H1 /\ H2) by Def10;
hence  x in H1 /\ H2 by STRUCT_0:def_5; ::_thesis: verum
end;

theorem :: GROUP_2:83
for G being Group
for H being strict Subgroup of G holds H /\ H = H
proof
let G be Group; ::_thesis: for H being strict Subgroup of G holds H /\ H = H
let H be strict Subgroup of G; ::_thesis: H /\ H = H
the carrier of (H /\ H) = (carr H) /\ (carr H) by Def10
.= the carrier of H ;
hence  H /\ H = H by Th59; ::_thesis: verum
end;

definition
let G be Group;
let H1, H2 be Subgroup of G;
:: original: /\
redefine funcH1 /\ H2 ->  strict Subgroup of G;
commutativity
 for H1, H2 being Subgroup of G holds H1 /\ H2 = H2 /\ H1
proof
let H1, H2 be Subgroup of G; ::_thesis: H1 /\ H2 = H2 /\ H1
the carrier of (H1 /\ H2) = (carr H2) /\ (carr H1) by Def10
.= the carrier of (H2 /\ H1) by Def10 ;
hence  H1 /\ H2 = H2 /\ H1 by Th59; ::_thesis: verum
end;
end;

theorem :: GROUP_2:84
for G being Group
for H1, H2, H3 being Subgroup of G holds (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3)
proof
let G be Group; ::_thesis: for H1, H2, H3 being Subgroup of G holds (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3)
let H1, H2, H3 be Subgroup of G; ::_thesis: (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3)
the carrier of ((H1 /\ H2) /\ H3) = (carr (H1 /\ H2)) /\ (carr H3) by Def10
.= ((carr H1) /\ (carr H2)) /\ (carr H3) by Def10
.= (carr H1) /\ ((carr H2) /\ (carr H3)) by XBOOLE_1:16
.= (carr H1) /\ (carr (H2 /\ H3)) by Def10
.= the carrier of (H1 /\ (H2 /\ H3)) by Def10 ;
hence  (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3) by Th59; ::_thesis: verum
end;

Lm3:  for G being Group
for H2, H1 being Subgroup of G holds
( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) )
proof
let G be Group; ::_thesis: for H2, H1 being Subgroup of G holds
( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) )
let H2, H1 be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) )
thus  ( H1 is Subgroup of H2 implies multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) ) ::_thesis: ( multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) implies H1 is Subgroup of H2 )
proof
assume  H1 is Subgroup of H2 ; ::_thesis: multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #)
then A1: the carrier of H1 c= the carrier of H2 by Def5;
 the carrier of (H1 /\ H2) = (carr H1) /\ (carr H2) by Def10;
hence  multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) by A1, Th59, XBOOLE_1:28; ::_thesis: verum
end;
assume  multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) ; ::_thesis: H1 is Subgroup of H2
then  the carrier of H1 = (carr H1) /\ (carr H2) by Def10
.= the carrier of H1 /\ the carrier of H2 ;
hence  H1 is Subgroup of H2 by Th57, XBOOLE_1:17; ::_thesis: verum
end;

theorem :: GROUP_2:85
for G being Group
for H being Subgroup of G holds
( ((1). G) /\ H = (1). G & H /\ ((1). G) = (1). G )
proof
let G be Group; ::_thesis: for H being Subgroup of G holds
( ((1). G) /\ H = (1). G & H /\ ((1). G) = (1). G )
let H be Subgroup of G; ::_thesis: ( ((1). G) /\ H = (1). G & H /\ ((1). G) = (1). G )
A1: (1). G is Subgroup of H by Th65;
hence  ((1). G) /\ H = (1). G by Lm3; ::_thesis: H /\ ((1). G) = (1). G
thus  H /\ ((1). G) = (1). G by A1, Lm3; ::_thesis: verum
end;

theorem :: GROUP_2:86
for G being strict Group
for H being strict Subgroup of G holds
( H /\ ((Omega). G) = H & ((Omega). G) /\ H = H ) by Lm3;

theorem :: GROUP_2:87
for G being strict Group holds ((Omega). G) /\ ((Omega). G) = G by Lm3;

Lm4:  for G being Group
for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1
let H1, H2 be Subgroup of G; ::_thesis: H1 /\ H2 is Subgroup of H1
 the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2 by Th80;
hence  H1 /\ H2 is Subgroup of H1 by Th57, XBOOLE_1:17; ::_thesis: verum
end;

theorem :: GROUP_2:88
for G being Group
for H1, H2 being Subgroup of G holds
( H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2 ) by Lm4;

theorem :: GROUP_2:89
for G being Group
for H2, H1 being Subgroup of G holds
( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) ) by Lm3;

theorem :: GROUP_2:90
for G being Group
for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds
H1 /\ H3 is Subgroup of H2
proof
let G be Group; ::_thesis: for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds
H1 /\ H3 is Subgroup of H2
let H1, H2, H3 be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2 )
assume A1: H1 is Subgroup of H2 ; ::_thesis: H1 /\ H3 is Subgroup of H2
 H1 /\ H3 is Subgroup of H1 by Lm4;
hence  H1 /\ H3 is Subgroup of H2 by A1, Th56; ::_thesis: verum
end;

theorem :: GROUP_2:91
for G being Group
for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 & H1 is Subgroup of H3 holds
H1 is Subgroup of H2 /\ H3
proof
let G be Group; ::_thesis: for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 & H1 is Subgroup of H3 holds
H1 is Subgroup of H2 /\ H3
let H1, H2, H3 be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 & H1 is Subgroup of H3 implies H1 is Subgroup of H2 /\ H3 )
assume A1: ( H1 is Subgroup of H2 & H1 is Subgroup of H3 ) ; ::_thesis: H1 is Subgroup of H2 /\ H3
now__::_thesis:_for_g_being_Element_of_G_st_g_in_H1_holds_
g_in_H2_/\_H3
let g be Element of G; ::_thesis: ( g in H1 implies g in H2 /\ H3 )
assume  g in H1 ; ::_thesis: g in H2 /\ H3
then  ( g in H2 & g in H3 ) by A1, Th40;
hence  g in H2 /\ H3 by Th82; ::_thesis: verum
end;
hence  H1 is Subgroup of H2 /\ H3 by Th58; ::_thesis: verum
end;

theorem :: GROUP_2:92
for G being Group
for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds
H1 /\ H3 is Subgroup of H2 /\ H3
proof
let G be Group; ::_thesis: for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds
H1 /\ H3 is Subgroup of H2 /\ H3
let H1, H2, H3 be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2 /\ H3 )
assume  H1 is Subgroup of H2 ; ::_thesis: H1 /\ H3 is Subgroup of H2 /\ H3
then  the carrier of H1 c= the carrier of H2 by Def5;
then  the carrier of H1 /\ the carrier of H3 c= the carrier of H2 /\ the carrier of H3 by XBOOLE_1:26;
then  the carrier of (H1 /\ H3) c= the carrier of H2 /\ the carrier of H3 by Th80;
then  the carrier of (H1 /\ H3) c= the carrier of (H2 /\ H3) by Th80;
hence  H1 /\ H3 is Subgroup of H2 /\ H3 by Th57; ::_thesis: verum
end;

theorem :: GROUP_2:93
for G being Group
for H1, H2 being Subgroup of G st ( H1 is finite or H2 is finite ) holds
H1 /\ H2 is finite
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G st ( H1 is finite or H2 is finite ) holds
H1 /\ H2 is finite
let H1, H2 be Subgroup of G; ::_thesis: ( ( H1 is finite or H2 is finite ) implies H1 /\ H2 is finite )
assume A1: ( H1 is finite or H2 is finite ) ; ::_thesis: H1 /\ H2 is finite
 ( H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2 ) by Lm4;
hence  H1 /\ H2 is finite by A1; ::_thesis: verum
end;

definition
let G be Group;
let H be Subgroup of G;
let A be Subset of G;
funcA * H ->  Subset of G equals :: GROUP_2:def 11
A * (carr H);
correctness
coherence
A * (carr H) is Subset of G;
;
funcH * A ->  Subset of G equals :: GROUP_2:def 12
(carr H) * A;
correctness
coherence
(carr H) * A is Subset of G;
;
end;

:: deftheorem  defines * GROUP_2:def_11_:_
 for G being Group
for H being Subgroup of G
for A being Subset of G holds A * H = A * (carr H);

:: deftheorem  defines * GROUP_2:def_12_:_
 for G being Group
for H being Subgroup of G
for A being Subset of G holds H * A = (carr H) * A;

theorem :: GROUP_2:94
for x being set
for G being Group
for A being Subset of G
for H being Subgroup of G holds
( x in A * H iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) )
proof
let x be set ; ::_thesis: for G being Group
for A being Subset of G
for H being Subgroup of G holds
( x in A * H iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) )
let G be Group; ::_thesis: for A being Subset of G
for H being Subgroup of G holds
( x in A * H iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) )
let A be Subset of G; ::_thesis: for H being Subgroup of G holds
( x in A * H iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) )
let H be Subgroup of G; ::_thesis: ( x in A * H iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) )
thus  ( x in A * H implies ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) ) ::_thesis: ( ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) implies x in A * H )
proof
assume  x in A * H ; ::_thesis: ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H )
then consider g1, g2 being Element of G such that
A1: ( x = g1 * g2 & g1 in A ) and
A2: g2 in carr H ;
 g2 in H by A2, STRUCT_0:def_5;
hence  ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in H ) by A1; ::_thesis: verum
end;
given g1, g2 being Element of G such that A3: ( x = g1 * g2 & g1 in A ) and
A4: g2 in H ; ::_thesis: x in A * H
 g2 in carr H by A4, STRUCT_0:def_5;
hence  x in A * H by A3; ::_thesis: verum
end;

theorem :: GROUP_2:95
for x being set
for G being Group
for A being Subset of G
for H being Subgroup of G holds
( x in H * A iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in H & g2 in A ) )
proof
let x be set ; ::_thesis: for G being Group
for A being Subset of G
for H being Subgroup of G holds
( x in H * A iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in H & g2 in A ) )
let G be Group; ::_thesis: for A being Subset of G
for H being Subgroup of G holds
( x in H * A iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in H & g2 in A ) )
let A be Subset of G; ::_thesis: for H being Subgroup of G holds
( x in H * A iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in H & g2 in A ) )
let H be Subgroup of G; ::_thesis: ( x in H * A iff ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in H & g2 in A ) )
thus  ( x in H * A implies ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in H & g2 in A ) ) ::_thesis: ( ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in H & g2 in A ) implies x in H * A )
proof
assume  x in H * A ; ::_thesis: ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in H & g2 in A )
then consider g1, g2 being Element of G such that
A1: x = g1 * g2 and
A2: g1 in carr H and
A3: g2 in A ;
 g1 in H by A2, STRUCT_0:def_5;
hence  ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in H & g2 in A ) by A1, A3; ::_thesis: verum
end;
given g1, g2 being Element of G such that A4: x = g1 * g2 and
A5: g1 in H and
A6: g2 in A ; ::_thesis: x in H * A
 g1 in carr H by A5, STRUCT_0:def_5;
hence  x in H * A by A4, A6; ::_thesis: verum
end;

theorem :: GROUP_2:96
for G being Group
for A, B being Subset of G
for H being Subgroup of G holds (A * B) * H = A * (B * H) by Th10;

theorem :: GROUP_2:97
for G being Group
for A, B being Subset of G
for H being Subgroup of G holds (A * H) * B = A * (H * B) by Th10;

theorem :: GROUP_2:98
for G being Group
for A, B being Subset of G
for H being Subgroup of G holds (H * A) * B = H * (A * B) by Th10;

theorem :: GROUP_2:99
for G being Group
for A being Subset of G
for H1, H2 being Subgroup of G holds (A * H1) * H2 = A * (H1 * (carr H2)) by Th10;

theorem :: GROUP_2:100
for G being Group
for A being Subset of G
for H1, H2 being Subgroup of G holds (H1 * A) * H2 = H1 * (A * H2) by Th10;

theorem :: GROUP_2:101
for G being Group
for A being Subset of G
for H1, H2 being Subgroup of G holds (H1 * (carr H2)) * A = H1 * (H2 * A) by Th10;

theorem :: GROUP_2:102
for G being Group
for A being Subset of G
for H being Subgroup of G st G is commutative Group holds
A * H = H * A by Th25;

definition
let G be Group;
let H be Subgroup of G;
let a be Element of G;
funca * H ->  Subset of G equals :: GROUP_2:def 13
a * (carr H);
correctness
coherence
a * (carr H) is Subset of G;
;
funcH * a ->  Subset of G equals :: GROUP_2:def 14
(carr H) * a;
correctness
coherence
(carr H) * a is Subset of G;
;
end;

:: deftheorem  defines * GROUP_2:def_13_:_
 for G being Group
for H being Subgroup of G
for a being Element of G holds a * H = a * (carr H);

:: deftheorem  defines * GROUP_2:def_14_:_
 for G being Group
for H being Subgroup of G
for a being Element of G holds H * a = (carr H) * a;

theorem Th103: :: GROUP_2:103
for x being set
for G being Group
for a being Element of G
for H being Subgroup of G holds
( x in a * H iff ex g being Element of G st
( x = a * g & g in H ) )
proof
let x be set ; ::_thesis: for G being Group
for a being Element of G
for H being Subgroup of G holds
( x in a * H iff ex g being Element of G st
( x = a * g & g in H ) )
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds
( x in a * H iff ex g being Element of G st
( x = a * g & g in H ) )
let a be Element of G; ::_thesis: for H being Subgroup of G holds
( x in a * H iff ex g being Element of G st
( x = a * g & g in H ) )
let H be Subgroup of G; ::_thesis: ( x in a * H iff ex g being Element of G st
( x = a * g & g in H ) )
thus  ( x in a * H implies ex g being Element of G st
( x = a * g & g in H ) ) ::_thesis: ( ex g being Element of G st
( x = a * g & g in H ) implies x in a * H )
proof
assume  x in a * H ; ::_thesis: ex g being Element of G st
( x = a * g & g in H )
then consider g being Element of G such that
A1: ( x = a * g & g in carr H ) by Th27;
take  g ; ::_thesis: ( x = a * g & g in H )
thus  ( x = a * g & g in H ) by A1, STRUCT_0:def_5; ::_thesis: verum
end;
given g being Element of G such that A2: x = a * g and
A3: g in H ; ::_thesis: x in a * H
 g in carr H by A3, STRUCT_0:def_5;
hence  x in a * H by A2, Th27; ::_thesis: verum
end;

theorem Th104: :: GROUP_2:104
for x being set
for G being Group
for a being Element of G
for H being Subgroup of G holds
( x in H * a iff ex g being Element of G st
( x = g * a & g in H ) )
proof
let x be set ; ::_thesis: for G being Group
for a being Element of G
for H being Subgroup of G holds
( x in H * a iff ex g being Element of G st
( x = g * a & g in H ) )
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds
( x in H * a iff ex g being Element of G st
( x = g * a & g in H ) )
let a be Element of G; ::_thesis: for H being Subgroup of G holds
( x in H * a iff ex g being Element of G st
( x = g * a & g in H ) )
let H be Subgroup of G; ::_thesis: ( x in H * a iff ex g being Element of G st
( x = g * a & g in H ) )
thus  ( x in H * a implies ex g being Element of G st
( x = g * a & g in H ) ) ::_thesis: ( ex g being Element of G st
( x = g * a & g in H ) implies x in H * a )
proof
assume  x in H * a ; ::_thesis: ex g being Element of G st
( x = g * a & g in H )
then consider g being Element of G such that
A1: ( x = g * a & g in carr H ) by Th28;
take  g ; ::_thesis: ( x = g * a & g in H )
thus  ( x = g * a & g in H ) by A1, STRUCT_0:def_5; ::_thesis: verum
end;
given g being Element of G such that A2: x = g * a and
A3: g in H ; ::_thesis: x in H * a
 g in carr H by A3, STRUCT_0:def_5;
hence  x in H * a by A2, Th28; ::_thesis: verum
end;

theorem :: GROUP_2:105
for G being Group
for a, b being Element of G
for H being Subgroup of G holds (a * b) * H = a * (b * H) by Th32;

theorem :: GROUP_2:106
for G being Group
for a, b being Element of G
for H being Subgroup of G holds (a * H) * b = a * (H * b) by Th10;

theorem :: GROUP_2:107
for G being Group
for a, b being Element of G
for H being Subgroup of G holds (H * a) * b = H * (a * b) by Th34;

theorem Th108: :: GROUP_2:108
for G being Group
for a being Element of G
for H being Subgroup of G holds
( a in a * H & a in H * a )
proof
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds
( a in a * H & a in H * a )
let a be Element of G; ::_thesis: for H being Subgroup of G holds
( a in a * H & a in H * a )
let H be Subgroup of G; ::_thesis: ( a in a * H & a in H * a )
A1: (1_ G) * a = a by GROUP_1:def_4;
 ( 1_ G in H & a * (1_ G) = a ) by Th46, GROUP_1:def_4;
hence  ( a in a * H & a in H * a ) by A1, Th103, Th104; ::_thesis: verum
end;

theorem :: GROUP_2:109
for G being Group
for H being Subgroup of G holds
( (1_ G) * H = carr H & H * (1_ G) = carr H ) by Th37;

theorem Th110: :: GROUP_2:110
for G being Group
for a being Element of G holds
( ((1). G) * a = {a} & a * ((1). G) = {a} )
proof
let G be Group; ::_thesis: for a being Element of G holds
( ((1). G) * a = {a} & a * ((1). G) = {a} )
let a be Element of G; ::_thesis: ( ((1). G) * a = {a} & a * ((1). G) = {a} )
A1: the carrier of ((1). G) = {(1_ G)} by Def7;
hence ((1). G) * a = {((1_ G) * a)} by Th18
.= {a} by GROUP_1:def_4 ;
::_thesis: a * ((1). G) = {a}
thus a * ((1). G) = {(a * (1_ G))} by A1, Th18
.= {a} by GROUP_1:def_4 ; ::_thesis: verum
end;

theorem Th111: :: GROUP_2:111
for G being Group
for a being Element of G holds
( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G )
proof
let G be Group; ::_thesis: for a being Element of G holds
( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G )
let a be Element of G; ::_thesis: ( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G )
 ([#] the carrier of G) * a = the carrier of G by Th17;
hence  ( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G ) by Th17; ::_thesis: verum
end;

theorem :: GROUP_2:112
for G being Group
for a being Element of G
for H being Subgroup of G st G is commutative Group holds
a * H = H * a by Th25;

theorem Th113: :: GROUP_2:113
for G being Group
for a being Element of G
for H being Subgroup of G holds
( a in H iff a * H = carr H )
proof
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds
( a in H iff a * H = carr H )
let a be Element of G; ::_thesis: for H being Subgroup of G holds
( a in H iff a * H = carr H )
let H be Subgroup of G; ::_thesis: ( a in H iff a * H = carr H )
thus  ( a in H implies a * H = carr H ) ::_thesis: ( a * H = carr H implies a in H )
proof
assume A1: a in H ; ::_thesis: a * H = carr H
thus  a * H c= carr H :: according to XBOOLE_0:def_10 ::_thesis: carr H c= a * H
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a * H or x in carr H )
assume  x in a * H ; ::_thesis: x in carr H
then consider g being Element of G such that
A2: x = a * g and
A3: g in H by Th103;
 a * g in H by A1, A3, Th50;
hence  x in carr H by A2, STRUCT_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in carr H or x in a * H )
assume A4: x in carr H ; ::_thesis: x in a * H
then A5: x in H by STRUCT_0:def_5;
reconsider b = x as Element of G by A4;
A6: a * ((a ") * b) = (a * (a ")) * b by GROUP_1:def_3
.= (1_ G) * b by GROUP_1:def_5
.= x by GROUP_1:def_4 ;
 a " in H by A1, Th51;
then  (a ") * b in H by A5, Th50;
hence  x in a * H by A6, Th103; ::_thesis: verum
end;
assume A7: a * H = carr H ; ::_thesis: a in H
 ( a * (1_ G) = a & 1_ G in H ) by Th46, GROUP_1:def_4;
then  a in carr H by A7, Th103;
hence  a in H by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th114: :: GROUP_2:114
for G being Group
for a, b being Element of G
for H being Subgroup of G holds
( a * H = b * H iff (b ") * a in H )
proof
let G be Group; ::_thesis: for a, b being Element of G
for H being Subgroup of G holds
( a * H = b * H iff (b ") * a in H )
let a, b be Element of G; ::_thesis: for H being Subgroup of G holds
( a * H = b * H iff (b ") * a in H )
let H be Subgroup of G; ::_thesis: ( a * H = b * H iff (b ") * a in H )
thus  ( a * H = b * H implies (b ") * a in H ) ::_thesis: ( (b ") * a in H implies a * H = b * H )
proof
assume A1: a * H = b * H ; ::_thesis: (b ") * a in H
((b ") * a) * H = (b ") * (a * H) by Th32
.= ((b ") * b) * H by A1, Th32
.= (1_ G) * H by GROUP_1:def_5
.= carr H by Th37 ;
hence  (b ") * a in H by Th113; ::_thesis: verum
end;
assume A2: (b ") * a in H ; ::_thesis: a * H = b * H
thus a * H = (1_ G) * (a * H) by Th37
.= ((1_ G) * a) * H by Th32
.= ((b * (b ")) * a) * H by GROUP_1:def_5
.= (b * ((b ") * a)) * H by GROUP_1:def_3
.= b * (((b ") * a) * H) by Th32
.= b * H by A2, Th113 ; ::_thesis: verum
end;

theorem Th115: :: GROUP_2:115
for G being Group
for a, b being Element of G
for H being Subgroup of G holds
( a * H = b * H iff a * H meets b * H )
proof
let G be Group; ::_thesis: for a, b being Element of G
for H being Subgroup of G holds
( a * H = b * H iff a * H meets b * H )
let a, b be Element of G; ::_thesis: for H being Subgroup of G holds
( a * H = b * H iff a * H meets b * H )
let H be Subgroup of G; ::_thesis: ( a * H = b * H iff a * H meets b * H )
 a * H <> {} by Th108;
hence  ( a * H = b * H implies a * H meets b * H ) by XBOOLE_1:66; ::_thesis: ( a * H meets b * H implies a * H = b * H )
assume  a * H meets b * H ; ::_thesis: a * H = b * H
then consider x being set  such that
A1: x in a * H and
A2: x in b * H by XBOOLE_0:3;
reconsider x = x as Element of G by A2;
consider g being Element of G such that
A3: x = a * g and
A4: g in H by A1, Th103;
A5: g " in H by A4, Th51;
consider h being Element of G such that
A6: x = b * h and
A7: h in H by A2, Th103;
a = (b * h) * (g ") by A3, A6, GROUP_1:14
.= b * (h * (g ")) by GROUP_1:def_3 ;
then  (b ") * a = h * (g ") by GROUP_1:13;
then  (b ") * a in H by A7, A5, Th50;
hence  a * H = b * H by Th114; ::_thesis: verum
end;

theorem Th116: :: GROUP_2:116
for G being Group
for a, b being Element of G
for H being Subgroup of G holds (a * b) * H c= (a * H) * (b * H)
proof
let G be Group; ::_thesis: for a, b being Element of G
for H being Subgroup of G holds (a * b) * H c= (a * H) * (b * H)
let a, b be Element of G; ::_thesis: for H being Subgroup of G holds (a * b) * H c= (a * H) * (b * H)
let H be Subgroup of G; ::_thesis: (a * b) * H c= (a * H) * (b * H)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (a * b) * H or x in (a * H) * (b * H) )
assume  x in (a * b) * H ; ::_thesis: x in (a * H) * (b * H)
then consider g being Element of G such that
A1: x = (a * b) * g and
A2: g in H by Th103;
A3: x = ((a * (1_ G)) * b) * g by A1, GROUP_1:def_4
.= (a * (1_ G)) * (b * g) by GROUP_1:def_3 ;
 1_ G in H by Th46;
then A4: a * (1_ G) in a * H by Th103;
 b * g in b * H by A2, Th103;
hence  x in (a * H) * (b * H) by A3, A4; ::_thesis: verum
end;

theorem :: GROUP_2:117
for G being Group
for a being Element of G
for H being Subgroup of G holds
( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) )
proof
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds
( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) )
let a be Element of G; ::_thesis: for H being Subgroup of G holds
( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) )
let H be Subgroup of G; ::_thesis: ( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) )
A1: ((a ") * a) * H = (1_ G) * H by GROUP_1:def_5
.= carr H by Th37 ;
(a * (a ")) * H = (1_ G) * H by GROUP_1:def_5
.= carr H by Th37 ;
hence  ( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) ) by A1, Th116; ::_thesis: verum
end;

theorem :: GROUP_2:118
for G being Group
for a being Element of G
for H being Subgroup of G holds (a |^ 2) * H c= (a * H) * (a * H)
proof
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds (a |^ 2) * H c= (a * H) * (a * H)
let a be Element of G; ::_thesis: for H being Subgroup of G holds (a |^ 2) * H c= (a * H) * (a * H)
let H be Subgroup of G; ::_thesis: (a |^ 2) * H c= (a * H) * (a * H)
 (a |^ 2) * H = (a * a) * H by GROUP_1:27;
hence  (a |^ 2) * H c= (a * H) * (a * H) by Th116; ::_thesis: verum
end;

theorem Th119: :: GROUP_2:119
for G being Group
for a being Element of G
for H being Subgroup of G holds
( a in H iff H * a = carr H )
proof
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds
( a in H iff H * a = carr H )
let a be Element of G; ::_thesis: for H being Subgroup of G holds
( a in H iff H * a = carr H )
let H be Subgroup of G; ::_thesis: ( a in H iff H * a = carr H )
thus  ( a in H implies H * a = carr H ) ::_thesis: ( H * a = carr H implies a in H )
proof
assume A1: a in H ; ::_thesis: H * a = carr H
thus  H * a c= carr H :: according to XBOOLE_0:def_10 ::_thesis: carr H c= H * a
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H * a or x in carr H )
assume  x in H * a ; ::_thesis: x in carr H
then consider g being Element of G such that
A2: x = g * a and
A3: g in H by Th104;
 g * a in H by A1, A3, Th50;
hence  x in carr H by A2, STRUCT_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in carr H or x in H * a )
assume A4: x in carr H ; ::_thesis: x in H * a
then A5: x in H by STRUCT_0:def_5;
reconsider b = x as Element of G by A4;
A6: (b * (a ")) * a = b * ((a ") * a) by GROUP_1:def_3
.= b * (1_ G) by GROUP_1:def_5
.= x by GROUP_1:def_4 ;
 a " in H by A1, Th51;
then  b * (a ") in H by A5, Th50;
hence  x in H * a by A6, Th104; ::_thesis: verum
end;
assume A7: H * a = carr H ; ::_thesis: a in H
 ( (1_ G) * a = a & 1_ G in H ) by Th46, GROUP_1:def_4;
then  a in carr H by A7, Th104;
hence  a in H by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th120: :: GROUP_2:120
for G being Group
for a, b being Element of G
for H being Subgroup of G holds
( H * a = H * b iff b * (a ") in H )
proof
let G be Group; ::_thesis: for a, b being Element of G
for H being Subgroup of G holds
( H * a = H * b iff b * (a ") in H )
let a, b be Element of G; ::_thesis: for H being Subgroup of G holds
( H * a = H * b iff b * (a ") in H )
let H be Subgroup of G; ::_thesis: ( H * a = H * b iff b * (a ") in H )
thus  ( H * a = H * b implies b * (a ") in H ) ::_thesis: ( b * (a ") in H implies H * a = H * b )
proof
assume A1: H * a = H * b ; ::_thesis: b * (a ") in H
carr H = H * (1_ G) by Th37
.= H * (a * (a ")) by GROUP_1:def_5
.= (H * b) * (a ") by A1, Th34
.= H * (b * (a ")) by Th34 ;
hence  b * (a ") in H by Th119; ::_thesis: verum
end;
assume  b * (a ") in H ; ::_thesis: H * a = H * b
hence H * a = (H * (b * (a "))) * a by Th119
.= H * ((b * (a ")) * a) by Th34
.= H * (b * ((a ") * a)) by GROUP_1:def_3
.= H * (b * (1_ G)) by GROUP_1:def_5
.= H * b by GROUP_1:def_4 ;
::_thesis: verum
end;

theorem :: GROUP_2:121
for G being Group
for a, b being Element of G
for H being Subgroup of G holds
( H * a = H * b iff H * a meets H * b )
proof
let G be Group; ::_thesis: for a, b being Element of G
for H being Subgroup of G holds
( H * a = H * b iff H * a meets H * b )
let a, b be Element of G; ::_thesis: for H being Subgroup of G holds
( H * a = H * b iff H * a meets H * b )
let H be Subgroup of G; ::_thesis: ( H * a = H * b iff H * a meets H * b )
 H * a <> {} by Th108;
hence  ( H * a = H * b implies H * a meets H * b ) by XBOOLE_1:66; ::_thesis: ( H * a meets H * b implies H * a = H * b )
assume  H * a meets H * b ; ::_thesis: H * a = H * b
then consider x being set  such that
A1: x in H * a and
A2: x in H * b by XBOOLE_0:3;
reconsider x = x as Element of G by A2;
consider g being Element of G such that
A3: x = g * a and
A4: g in H by A1, Th104;
A5: g " in H by A4, Th51;
consider h being Element of G such that
A6: x = h * b and
A7: h in H by A2, Th104;
a = (g ") * (h * b) by A3, A6, GROUP_1:13
.= ((g ") * h) * b by GROUP_1:def_3 ;
then  a * (b ") = (g ") * h by GROUP_1:14;
then  a * (b ") in H by A7, A5, Th50;
hence  H * a = H * b by Th120; ::_thesis: verum
end;

theorem Th122: :: GROUP_2:122
for G being Group
for a, b being Element of G
for H being Subgroup of G holds (H * a) * b c= (H * a) * (H * b)
proof
let G be Group; ::_thesis: for a, b being Element of G
for H being Subgroup of G holds (H * a) * b c= (H * a) * (H * b)
let a, b be Element of G; ::_thesis: for H being Subgroup of G holds (H * a) * b c= (H * a) * (H * b)
let H be Subgroup of G; ::_thesis: (H * a) * b c= (H * a) * (H * b)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (H * a) * b or x in (H * a) * (H * b) )
 1_ G in H by Th46;
then A1: (1_ G) * b in H * b by Th104;
assume  x in (H * a) * b ; ::_thesis: x in (H * a) * (H * b)
then  x in H * (a * b) by Th34;
then consider g being Element of G such that
A2: x = g * (a * b) and
A3: g in H by Th104;
A4: x = (g * a) * b by A2, GROUP_1:def_3
.= (g * a) * ((1_ G) * b) by GROUP_1:def_4 ;
 g * a in H * a by A3, Th104;
hence  x in (H * a) * (H * b) by A1, A4; ::_thesis: verum
end;

theorem :: GROUP_2:123
for G being Group
for a being Element of G
for H being Subgroup of G holds
( carr H c= (H * a) * (H * (a ")) & carr H c= (H * (a ")) * (H * a) )
proof
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds
( carr H c= (H * a) * (H * (a ")) & carr H c= (H * (a ")) * (H * a) )
let a be Element of G; ::_thesis: for H being Subgroup of G holds
( carr H c= (H * a) * (H * (a ")) & carr H c= (H * (a ")) * (H * a) )
let H be Subgroup of G; ::_thesis: ( carr H c= (H * a) * (H * (a ")) & carr H c= (H * (a ")) * (H * a) )
A1: (H * (a ")) * a = H * ((a ") * a) by Th34
.= H * (1_ G) by GROUP_1:def_5
.= carr H by Th37 ;
(H * a) * (a ") = H * (a * (a ")) by Th34
.= H * (1_ G) by GROUP_1:def_5
.= carr H by Th37 ;
hence  ( carr H c= (H * a) * (H * (a ")) & carr H c= (H * (a ")) * (H * a) ) by A1, Th122; ::_thesis: verum
end;

theorem :: GROUP_2:124
for G being Group
for a being Element of G
for H being Subgroup of G holds H * (a |^ 2) c= (H * a) * (H * a)
proof
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds H * (a |^ 2) c= (H * a) * (H * a)
let a be Element of G; ::_thesis: for H being Subgroup of G holds H * (a |^ 2) c= (H * a) * (H * a)
let H be Subgroup of G; ::_thesis: H * (a |^ 2) c= (H * a) * (H * a)
 ( a |^ 2 = a * a & (H * a) * a = H * (a * a) ) by Th34, GROUP_1:27;
hence  H * (a |^ 2) c= (H * a) * (H * a) by Th122; ::_thesis: verum
end;

theorem :: GROUP_2:125
for G being Group
for a being Element of G
for H1, H2 being Subgroup of G holds a * (H1 /\ H2) = (a * H1) /\ (a * H2)
proof
let G be Group; ::_thesis: for a being Element of G
for H1, H2 being Subgroup of G holds a * (H1 /\ H2) = (a * H1) /\ (a * H2)
let a be Element of G; ::_thesis: for H1, H2 being Subgroup of G holds a * (H1 /\ H2) = (a * H1) /\ (a * H2)
let H1, H2 be Subgroup of G; ::_thesis: a * (H1 /\ H2) = (a * H1) /\ (a * H2)
thus  a * (H1 /\ H2) c= (a * H1) /\ (a * H2) :: according to XBOOLE_0:def_10 ::_thesis: (a * H1) /\ (a * H2) c= a * (H1 /\ H2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a * (H1 /\ H2) or x in (a * H1) /\ (a * H2) )
assume  x in a * (H1 /\ H2) ; ::_thesis: x in (a * H1) /\ (a * H2)
then consider g being Element of G such that
A1: x = a * g and
A2: g in H1 /\ H2 by Th103;
 g in H2 by A2, Th82;
then A3: x in a * H2 by A1, Th103;
 g in H1 by A2, Th82;
then  x in a * H1 by A1, Th103;
hence  x in (a * H1) /\ (a * H2) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (a * H1) /\ (a * H2) or x in a * (H1 /\ H2) )
assume A4: x in (a * H1) /\ (a * H2) ; ::_thesis: x in a * (H1 /\ H2)
then  x in a * H1 by XBOOLE_0:def_4;
then consider g being Element of G such that
A5: x = a * g and
A6: g in H1 by Th103;
 x in a * H2 by A4, XBOOLE_0:def_4;
then consider g1 being Element of G such that
A7: x = a * g1 and
A8: g1 in H2 by Th103;
 g = g1 by A5, A7, GROUP_1:6;
then  g in H1 /\ H2 by A6, A8, Th82;
hence  x in a * (H1 /\ H2) by A5, Th103; ::_thesis: verum
end;

theorem :: GROUP_2:126
for G being Group
for a being Element of G
for H1, H2 being Subgroup of G holds (H1 /\ H2) * a = (H1 * a) /\ (H2 * a)
proof
let G be Group; ::_thesis: for a being Element of G
for H1, H2 being Subgroup of G holds (H1 /\ H2) * a = (H1 * a) /\ (H2 * a)
let a be Element of G; ::_thesis: for H1, H2 being Subgroup of G holds (H1 /\ H2) * a = (H1 * a) /\ (H2 * a)
let H1, H2 be Subgroup of G; ::_thesis: (H1 /\ H2) * a = (H1 * a) /\ (H2 * a)
thus  (H1 /\ H2) * a c= (H1 * a) /\ (H2 * a) :: according to XBOOLE_0:def_10 ::_thesis: (H1 * a) /\ (H2 * a) c= (H1 /\ H2) * a
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (H1 /\ H2) * a or x in (H1 * a) /\ (H2 * a) )
assume  x in (H1 /\ H2) * a ; ::_thesis: x in (H1 * a) /\ (H2 * a)
then consider g being Element of G such that
A1: x = g * a and
A2: g in H1 /\ H2 by Th104;
 g in H2 by A2, Th82;
then A3: x in H2 * a by A1, Th104;
 g in H1 by A2, Th82;
then  x in H1 * a by A1, Th104;
hence  x in (H1 * a) /\ (H2 * a) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (H1 * a) /\ (H2 * a) or x in (H1 /\ H2) * a )
assume A4: x in (H1 * a) /\ (H2 * a) ; ::_thesis: x in (H1 /\ H2) * a
then  x in H1 * a by XBOOLE_0:def_4;
then consider g being Element of G such that
A5: x = g * a and
A6: g in H1 by Th104;
 x in H2 * a by A4, XBOOLE_0:def_4;
then consider g1 being Element of G such that
A7: x = g1 * a and
A8: g1 in H2 by Th104;
 g = g1 by A5, A7, GROUP_1:6;
then  g in H1 /\ H2 by A6, A8, Th82;
hence  x in (H1 /\ H2) * a by A5, Th104; ::_thesis: verum
end;

theorem :: GROUP_2:127
for G being Group
for a being Element of G
for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")
proof
let G be Group; ::_thesis: for a being Element of G
for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")
let a be Element of G; ::_thesis: for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")
let H2 be Subgroup of G; ::_thesis: ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")
set A = (a * H2) * (a ");
set x = the Element of a * H2;
A1: a * H2 <> {} by Th108;
then reconsider x = the Element of a * H2 as Element of G by Lm1;
A2: now__::_thesis:_for_g_being_Element_of_G_st_g_in_(a_*_H2)_*_(a_")_holds_
g_"_in_(a_*_H2)_*_(a_")
let g be Element of G; ::_thesis: ( g in (a * H2) * (a ") implies g " in (a * H2) * (a ") )
assume  g in (a * H2) * (a ") ; ::_thesis: g " in (a * H2) * (a ")
then consider g1 being Element of G such that
A3: g = g1 * (a ") and
A4: g1 in a * H2 by Th28;
consider g2 being Element of G such that
A5: g1 = a * g2 and
A6: g2 in H2 by A4, Th103;
 g2 " in H2 by A6, Th51;
then A7: (g2 ") * (a ") in H2 * (a ") by Th104;
g " = ((a ") ") * ((a * g2) ") by A3, A5, GROUP_1:17
.= a * ((g2 ") * (a ")) by GROUP_1:17 ;
then  g " in a * (H2 * (a ")) by A7, Th27;
hence  g " in (a * H2) * (a ") by Th10; ::_thesis: verum
end;
A8: now__::_thesis:_for_g1,_g2_being_Element_of_G_st_g1_in_(a_*_H2)_*_(a_")_&_g2_in_(a_*_H2)_*_(a_")_holds_
g1_*_g2_in_(a_*_H2)_*_(a_")
let g1, g2 be Element of G; ::_thesis: ( g1 in (a * H2) * (a ") & g2 in (a * H2) * (a ") implies g1 * g2 in (a * H2) * (a ") )
assume that
A9: g1 in (a * H2) * (a ") and
A10: g2 in (a * H2) * (a ") ; ::_thesis: g1 * g2 in (a * H2) * (a ")
consider g being Element of G such that
A11: g1 = g * (a ") and
A12: g in a * H2 by A9, Th28;
consider h being Element of G such that
A13: g = a * h and
A14: h in H2 by A12, Th103;
 (a * H2) * (a ") = a * (H2 * (a ")) by Th10;
then consider b being Element of G such that
A15: g2 = a * b and
A16: b in H2 * (a ") by A10, Th27;
consider c being Element of G such that
A17: b = c * (a ") and
A18: c in H2 by A16, Th104;
 h * c in H2 by A14, A18, Th50;
then A19: a * (h * c) in a * H2 by Th103;
g1 * g2 = (a * h) * ((a ") * (a * (c * (a ")))) by A11, A15, A13, A17, GROUP_1:def_3
.= (a * h) * (((a ") * a) * (c * (a "))) by GROUP_1:def_3
.= (a * h) * ((1_ G) * (c * (a "))) by GROUP_1:def_5
.= (a * h) * (c * (a ")) by GROUP_1:def_4
.= ((a * h) * c) * (a ") by GROUP_1:def_3
.= (a * (h * c)) * (a ") by GROUP_1:def_3 ;
hence  g1 * g2 in (a * H2) * (a ") by A19, Th28; ::_thesis: verum
end;
 x * (a ") in (a * H2) * (a ") by A1, Th28;
hence  ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ") by A8, A2, Th52; ::_thesis: verum
end;

theorem Th128: :: GROUP_2:128
for G being Group
for a, b being Element of G
for H being Subgroup of G holds a * H,b * H are_equipotent
proof
let G be Group; ::_thesis: for a, b being Element of G
for H being Subgroup of G holds a * H,b * H are_equipotent
let a, b be Element of G; ::_thesis: for H being Subgroup of G holds a * H,b * H are_equipotent
let H be Subgroup of G; ::_thesis: a * H,b * H are_equipotent
defpred S1[ set , set ] means  ex g1 being Element of G st
( $1 = g1 & $2 = (b * (a ")) * g1 );
A1: for x being set st x in a * H holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in a * H implies ex y being set st S1[x,y] )
assume  x in a * H ; ::_thesis: ex y being set st S1[x,y]
then reconsider g = x as Element of G ;
reconsider y = (b * (a ")) * g as set ;
take  y ; ::_thesis: S1[x,y]
take  g ; ::_thesis: ( x = g & y = (b * (a ")) * g )
thus  ( x = g & y = (b * (a ")) * g ) ; ::_thesis: verum
end;
consider f being Function such that
A2: dom f = a * H and
A3: for x being set st x in a * H holds
S1[x,f . x] from CLASSES1:sch_1(A1);
A4: rng f = b * H
proof
thus  rng f c= b * H :: according to XBOOLE_0:def_10 ::_thesis: b * H c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in b * H )
assume  x in rng f ; ::_thesis: x in b * H
then consider y being set  such that
A5: y in dom f and
A6: f . y = x by FUNCT_1:def_3;
consider g being Element of G such that
A7: y = g and
A8: x = (b * (a ")) * g by A2, A3, A5, A6;
consider g1 being Element of G such that
A9: g = a * g1 and
A10: g1 in H by A2, A5, A7, Th103;
x = ((b * (a ")) * a) * g1 by A8, A9, GROUP_1:def_3
.= (b * ((a ") * a)) * g1 by GROUP_1:def_3
.= (b * (1_ G)) * g1 by GROUP_1:def_5
.= b * g1 by GROUP_1:def_4 ;
hence  x in b * H by A10, Th103; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in b * H or x in rng f )
assume  x in b * H ; ::_thesis: x in rng f
then consider g being Element of G such that
A11: x = b * g and
A12: g in H by Th103;
A13: a * g in dom f by A2, A12, Th103;
then  ex g1 being Element of G st
( g1 = a * g & f . (a * g) = (b * (a ")) * g1 ) by A2, A3;
then f . (a * g) = ((b * (a ")) * a) * g by GROUP_1:def_3
.= (b * ((a ") * a)) * g by GROUP_1:def_3
.= (b * (1_ G)) * g by GROUP_1:def_5
.= x by A11, GROUP_1:def_4 ;
hence  x in rng f by A13, FUNCT_1:def_3; ::_thesis: verum
end;
 f is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A14: ( x in dom f & y in dom f ) and
A15: f . x = f . y ; ::_thesis: x = y
 ( ex g1 being Element of G st
( x = g1 & f . x = (b * (a ")) * g1 ) & ex g2 being Element of G st
( y = g2 & f . y = (b * (a ")) * g2 ) ) by A2, A3, A14;
hence  x = y by A15, GROUP_1:6; ::_thesis: verum
end;
hence  a * H,b * H are_equipotent by A2, A4, WELLORD2:def_4; ::_thesis: verum
end;

theorem Th129: :: GROUP_2:129
for G being Group
for a, b being Element of G
for H being Subgroup of G holds a * H,H * b are_equipotent
proof
let G be Group; ::_thesis: for a, b being Element of G
for H being Subgroup of G holds a * H,H * b are_equipotent
let a, b be Element of G; ::_thesis: for H being Subgroup of G holds a * H,H * b are_equipotent
let H be Subgroup of G; ::_thesis: a * H,H * b are_equipotent
defpred S1[ set , set ] means  ex g1 being Element of G st
( $1 = g1 & $2 = ((a ") * g1) * b );
A1: for x being set st x in a * H holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in a * H implies ex y being set st S1[x,y] )
assume  x in a * H ; ::_thesis: ex y being set st S1[x,y]
then reconsider g = x as Element of G ;
reconsider y = ((a ") * g) * b as set ;
take  y ; ::_thesis: S1[x,y]
take  g ; ::_thesis: ( x = g & y = ((a ") * g) * b )
thus  ( x = g & y = ((a ") * g) * b ) ; ::_thesis: verum
end;
consider f being Function such that
A2: dom f = a * H and
A3: for x being set st x in a * H holds
S1[x,f . x] from CLASSES1:sch_1(A1);
A4: rng f = H * b
proof
thus  rng f c= H * b :: according to XBOOLE_0:def_10 ::_thesis: H * b c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in H * b )
assume  x in rng f ; ::_thesis: x in H * b
then consider y being set  such that
A5: y in dom f and
A6: f . y = x by FUNCT_1:def_3;
consider g being Element of G such that
A7: y = g and
A8: x = ((a ") * g) * b by A2, A3, A5, A6;
consider g1 being Element of G such that
A9: g = a * g1 and
A10: g1 in H by A2, A5, A7, Th103;
x = (((a ") * a) * g1) * b by A8, A9, GROUP_1:def_3
.= ((1_ G) * g1) * b by GROUP_1:def_5
.= g1 * b by GROUP_1:def_4 ;
hence  x in H * b by A10, Th104; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H * b or x in rng f )
assume  x in H * b ; ::_thesis: x in rng f
then consider g being Element of G such that
A11: x = g * b and
A12: g in H by Th104;
A13: a * g in dom f by A2, A12, Th103;
then  ex g1 being Element of G st
( g1 = a * g & f . (a * g) = ((a ") * g1) * b ) by A2, A3;
then f . (a * g) = (((a ") * a) * g) * b by GROUP_1:def_3
.= ((1_ G) * g) * b by GROUP_1:def_5
.= x by A11, GROUP_1:def_4 ;
hence  x in rng f by A13, FUNCT_1:def_3; ::_thesis: verum
end;
 f is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A14: x in dom f and
A15: y in dom f and
A16: f . x = f . y ; ::_thesis: x = y
consider g2 being Element of G such that
A17: y = g2 and
A18: f . y = ((a ") * g2) * b by A2, A3, A15;
consider g1 being Element of G such that
A19: x = g1 and
A20: f . x = ((a ") * g1) * b by A2, A3, A14;
 (a ") * g1 = (a ") * g2 by A16, A20, A18, GROUP_1:6;
hence  x = y by A19, A17, GROUP_1:6; ::_thesis: verum
end;
hence  a * H,H * b are_equipotent by A2, A4, WELLORD2:def_4; ::_thesis: verum
end;

theorem Th130: :: GROUP_2:130
for G being Group
for a, b being Element of G
for H being Subgroup of G holds H * a,H * b are_equipotent
proof
let G be Group; ::_thesis: for a, b being Element of G
for H being Subgroup of G holds H * a,H * b are_equipotent
let a, b be Element of G; ::_thesis: for H being Subgroup of G holds H * a,H * b are_equipotent
let H be Subgroup of G; ::_thesis: H * a,H * b are_equipotent
 ( H * a,b * H are_equipotent & b * H,H * b are_equipotent ) by Th129;
hence  H * a,H * b are_equipotent by WELLORD2:15; ::_thesis: verum
end;

theorem Th131: :: GROUP_2:131
for G being Group
for a being Element of G
for H being Subgroup of G holds
( carr H,a * H are_equipotent & carr H,H * a are_equipotent )
proof
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds
( carr H,a * H are_equipotent & carr H,H * a are_equipotent )
let a be Element of G; ::_thesis: for H being Subgroup of G holds
( carr H,a * H are_equipotent & carr H,H * a are_equipotent )
let H be Subgroup of G; ::_thesis: ( carr H,a * H are_equipotent & carr H,H * a are_equipotent )
 ( carr H = (1_ G) * H & carr H = H * (1_ G) ) by Th37;
hence  ( carr H,a * H are_equipotent & carr H,H * a are_equipotent ) by Th128, Th130; ::_thesis: verum
end;

theorem :: GROUP_2:132
for G being Group
for a being Element of G
for H being Subgroup of G holds
( card H = card (a * H) & card H = card (H * a) )
proof
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G holds
( card H = card (a * H) & card H = card (H * a) )
let a be Element of G; ::_thesis: for H being Subgroup of G holds
( card H = card (a * H) & card H = card (H * a) )
let H be Subgroup of G; ::_thesis: ( card H = card (a * H) & card H = card (H * a) )
 carr H,a * H are_equipotent by Th131;
hence  card H = card (a * H) by CARD_1:5; ::_thesis: card H = card (H * a)
 carr H,H * a are_equipotent by Th131;
hence  card H = card (H * a) by CARD_1:5; ::_thesis: verum
end;

theorem Th133: :: GROUP_2:133
for G being Group
for a being Element of G
for H being finite Subgroup of G ex B, C being finite set st
( B = a * H & C = H * a & card H = card B & card H = card C )
proof
let G be Group; ::_thesis: for a being Element of G
for H being finite Subgroup of G ex B, C being finite set st
( B = a * H & C = H * a & card H = card B & card H = card C )
let a be Element of G; ::_thesis: for H being finite Subgroup of G ex B, C being finite set st
( B = a * H & C = H * a & card H = card B & card H = card C )
let H be finite Subgroup of G; ::_thesis: ex B, C being finite set st
( B = a * H & C = H * a & card H = card B & card H = card C )
reconsider B = a * H, C = H * a as finite set by Th131, CARD_1:38;
take  B ; ::_thesis: ex C being finite set st
( B = a * H & C = H * a & card H = card B & card H = card C )
take  C ; ::_thesis: ( B = a * H & C = H * a & card H = card B & card H = card C )
 ( carr H,a * H are_equipotent & carr H,H * a are_equipotent ) by Th131;
hence  ( B = a * H & C = H * a & card H = card B & card H = card C ) by CARD_1:5; ::_thesis: verum
end;

definition
let G be Group;
let H be Subgroup of G;
func Left_Cosets H ->  Subset-Family of G means :Def15: :: GROUP_2:def 15
 for A being Subset of G holds
( A in it iff ex a being Element of G st A = a * H );
existence
 ex b1 being Subset-Family of G st
for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = a * H )
proof
defpred S1[ set ] means  ex a being Element of G st $1 = a * H;
 ex F being Subset-Family of G st
for A being Subset of G holds
( A in F iff S1[A] ) from SUBSET_1:sch_3();
hence  ex b1 being Subset-Family of G st
for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = a * H ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of G st ( for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = a * H ) ) & ( for A being Subset of G holds
( A in b2 iff ex a being Element of G st A = a * H ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex a being Element of G st $1 = a * H;
let F1, F2 be Subset-Family of G; ::_thesis: ( ( for A being Subset of G holds
( A in F1 iff ex a being Element of G st A = a * H ) ) & ( for A being Subset of G holds
( A in F2 iff ex a being Element of G st A = a * H ) ) implies F1 = F2 )
assume A1: for A being Subset of G holds
( A in F1 iff S1[A] ) ; ::_thesis: ( ex A being Subset of G st
( ( A in F2 implies ex a being Element of G st A = a * H ) implies ( ex a being Element of G st A = a * H & not A in F2 ) ) or F1 = F2 )
assume A2: for A being Subset of G holds
( A in F2 iff S1[A] ) ; ::_thesis: F1 = F2
thus  F1 = F2 from SUBSET_1:sch_4(A1, A2); ::_thesis: verum
end;
func Right_Cosets H ->  Subset-Family of G means :Def16: :: GROUP_2:def 16
 for A being Subset of G holds
( A in it iff ex a being Element of G st A = H * a );
existence
 ex b1 being Subset-Family of G st
for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = H * a )
proof
defpred S1[ set ] means  ex a being Element of G st $1 = H * a;
 ex F being Subset-Family of G st
for A being Subset of G holds
( A in F iff S1[A] ) from SUBSET_1:sch_3();
hence  ex b1 being Subset-Family of G st
for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = H * a ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of G st ( for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = H * a ) ) & ( for A being Subset of G holds
( A in b2 iff ex a being Element of G st A = H * a ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex a being Element of G st $1 = H * a;
let F1, F2 be Subset-Family of G; ::_thesis: ( ( for A being Subset of G holds
( A in F1 iff ex a being Element of G st A = H * a ) ) & ( for A being Subset of G holds
( A in F2 iff ex a being Element of G st A = H * a ) ) implies F1 = F2 )
assume A3: for A being Subset of G holds
( A in F1 iff S1[A] ) ; ::_thesis: ( ex A being Subset of G st
( ( A in F2 implies ex a being Element of G st A = H * a ) implies ( ex a being Element of G st A = H * a & not A in F2 ) ) or F1 = F2 )
assume A4: for A being Subset of G holds
( A in F2 iff S1[A] ) ; ::_thesis: F1 = F2
thus  F1 = F2 from SUBSET_1:sch_4(A3, A4); ::_thesis: verum
end;
end;

:: deftheorem Def15 defines Left_Cosets GROUP_2:def_15_:_
 for G being Group
for H being Subgroup of G
for b3 being Subset-Family of G holds
( b3 = Left_Cosets H iff for A being Subset of G holds
( A in b3 iff ex a being Element of G st A = a * H ) );

:: deftheorem Def16 defines Right_Cosets GROUP_2:def_16_:_
 for G being Group
for H being Subgroup of G
for b3 being Subset-Family of G holds
( b3 = Right_Cosets H iff for A being Subset of G holds
( A in b3 iff ex a being Element of G st A = H * a ) );

theorem :: GROUP_2:134
for G being Group
for H being Subgroup of G st G is finite holds
( Right_Cosets H is finite & Left_Cosets H is finite ) ;

theorem :: GROUP_2:135
for G being Group
for H being Subgroup of G holds
( carr H in Left_Cosets H & carr H in Right_Cosets H )
proof
let G be Group; ::_thesis: for H being Subgroup of G holds
( carr H in Left_Cosets H & carr H in Right_Cosets H )
let H be Subgroup of G; ::_thesis: ( carr H in Left_Cosets H & carr H in Right_Cosets H )
 ( carr H = (1_ G) * H & carr H = H * (1_ G) ) by Th37;
hence  ( carr H in Left_Cosets H & carr H in Right_Cosets H ) by Def15, Def16; ::_thesis: verum
end;

theorem Th136: :: GROUP_2:136
for G being Group
for H being Subgroup of G holds Left_Cosets H, Right_Cosets H are_equipotent
proof
let G be Group; ::_thesis: for H being Subgroup of G holds Left_Cosets H, Right_Cosets H are_equipotent
let H be Subgroup of G; ::_thesis: Left_Cosets H, Right_Cosets H are_equipotent
defpred S1[ set , set ] means  ex g being Element of G st
( $1 = g * H & $2 = H * (g ") );
A1: for x being set st x in Left_Cosets H holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in Left_Cosets H implies ex y being set st S1[x,y] )
assume  x in Left_Cosets H ; ::_thesis: ex y being set st S1[x,y]
then consider g being Element of G such that
A2: x = g * H by Def15;
reconsider y = H * (g ") as set ;
take  y ; ::_thesis: S1[x,y]
take  g ; ::_thesis: ( x = g * H & y = H * (g ") )
thus  ( x = g * H & y = H * (g ") ) by A2; ::_thesis: verum
end;
consider f being Function such that
A3: dom f = Left_Cosets H and
A4: for x being set st x in Left_Cosets H holds
S1[x,f . x] from CLASSES1:sch_1(A1);
A5: rng f = Right_Cosets H
proof
thus  rng f c= Right_Cosets H :: according to XBOOLE_0:def_10 ::_thesis: Right_Cosets H c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Right_Cosets H )
assume  x in rng f ; ::_thesis: x in Right_Cosets H
then consider y being set  such that
A6: y in dom f and
A7: f . y = x by FUNCT_1:def_3;
 ex g being Element of G st
( y = g * H & f . y = H * (g ") ) by A3, A4, A6;
hence  x in Right_Cosets H by A7, Def16; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Right_Cosets H or x in rng f )
assume A8: x in Right_Cosets H ; ::_thesis: x in rng f
then reconsider A = x as Subset of G ;
consider g being Element of G such that
A9: A = H * g by A8, Def16;
A10: (g ") * H in Left_Cosets H by Def15;
then A11: f . ((g ") * H) in rng f by A3, FUNCT_1:def_3;
consider a being Element of G such that
A12: (g ") * H = a * H and
A13: f . ((g ") * H) = H * (a ") by A4, A10;
 (a ") * (g ") in H by A12, Th114;
hence  x in rng f by A9, A11, A13, Th120; ::_thesis: verum
end;
 f is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A14: x in dom f and
A15: y in dom f and
A16: f . x = f . y ; ::_thesis: x = y
consider b being Element of G such that
A17: y = b * H and
A18: f . y = H * (b ") by A3, A4, A15;
consider a being Element of G such that
A19: x = a * H and
A20: f . x = H * (a ") by A3, A4, A14;
 (b ") * ((a ") ") in H by A16, A20, A18, Th120;
hence  x = y by A19, A17, Th114; ::_thesis: verum
end;
hence  Left_Cosets H, Right_Cosets H are_equipotent by A3, A5, WELLORD2:def_4; ::_thesis: verum
end;

theorem Th137: :: GROUP_2:137
for G being Group
for H being Subgroup of G holds
( union (Left_Cosets H) = the carrier of G & union (Right_Cosets H) = the carrier of G )
proof
let G be Group; ::_thesis: for H being Subgroup of G holds
( union (Left_Cosets H) = the carrier of G & union (Right_Cosets H) = the carrier of G )
let H be Subgroup of G; ::_thesis: ( union (Left_Cosets H) = the carrier of G & union (Right_Cosets H) = the carrier of G )
thus  union (Left_Cosets H) = the carrier of G ::_thesis: union (Right_Cosets H) = the carrier of G
proof
set h = the Element of H;
reconsider g = the Element of H as Element of G by Th42;
thus  union (Left_Cosets H) c= the carrier of G ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of G c= union (Left_Cosets H)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of G or x in union (Left_Cosets H) )
assume  x in the carrier of G ; ::_thesis: x in union (Left_Cosets H)
then reconsider a = x as Element of G ;
A1: a = a * (1_ G) by GROUP_1:def_4
.= a * ((g ") * g) by GROUP_1:def_5
.= (a * (g ")) * g by GROUP_1:def_3 ;
A2: (a * (g ")) * H in Left_Cosets H by Def15;
 the Element of H in H by STRUCT_0:def_5;
then  a in (a * (g ")) * H by A1, Th103;
hence  x in union (Left_Cosets H) by A2, TARSKI:def_4; ::_thesis: verum
end;
set h = the Element of H;
reconsider g = the Element of H as Element of G by Th42;
thus  union (Right_Cosets H) c= the carrier of G ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of G c= union (Right_Cosets H)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of G or x in union (Right_Cosets H) )
assume  x in the carrier of G ; ::_thesis: x in union (Right_Cosets H)
then reconsider a = x as Element of G ;
A3: a = (1_ G) * a by GROUP_1:def_4
.= (g * (g ")) * a by GROUP_1:def_5
.= g * ((g ") * a) by GROUP_1:def_3 ;
A4: H * ((g ") * a) in Right_Cosets H by Def16;
 the Element of H in H by STRUCT_0:def_5;
then  a in H * ((g ") * a) by A3, Th104;
hence  x in union (Right_Cosets H) by A4, TARSKI:def_4; ::_thesis: verum
end;

theorem Th138: :: GROUP_2:138
for G being Group holds Left_Cosets ((1). G) =  {  {a} where a is Element of G : verum  }
proof
let G be Group; ::_thesis: Left_Cosets ((1). G) =  {  {a} where a is Element of G : verum  }
set A =  {  {a} where a is Element of G : verum  }  ;
thus  Left_Cosets ((1). G) c=  {  {a} where a is Element of G : verum  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  {a} where a is Element of G : verum  }  c= Left_Cosets ((1). G)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Left_Cosets ((1). G) or x in  {  {a} where a is Element of G : verum  }  )
assume A1: x in Left_Cosets ((1). G) ; ::_thesis: x in  {  {a} where a is Element of G : verum  }
then reconsider X = x as Subset of G ;
consider g being Element of G such that
A2: X = g * ((1). G) by A1, Def15;
 x = {g} by A2, Th110;
hence  x in  {  {a} where a is Element of G : verum  }  ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  {a} where a is Element of G : verum  }  or x in Left_Cosets ((1). G) )
assume  x in  {  {a} where a is Element of G : verum  }  ; ::_thesis: x in Left_Cosets ((1). G)
then consider a being Element of G such that
A3: x = {a} ;
 a * ((1). G) = {a} by Th110;
hence  x in Left_Cosets ((1). G) by A3, Def15; ::_thesis: verum
end;

theorem :: GROUP_2:139
for G being Group holds Right_Cosets ((1). G) =  {  {a} where a is Element of G : verum  }
proof
let G be Group; ::_thesis: Right_Cosets ((1). G) =  {  {a} where a is Element of G : verum  }
set A =  {  {a} where a is Element of G : verum  }  ;
thus  Right_Cosets ((1). G) c=  {  {a} where a is Element of G : verum  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  {a} where a is Element of G : verum  }  c= Right_Cosets ((1). G)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Right_Cosets ((1). G) or x in  {  {a} where a is Element of G : verum  }  )
assume A1: x in Right_Cosets ((1). G) ; ::_thesis: x in  {  {a} where a is Element of G : verum  }
then reconsider X = x as Subset of G ;
consider g being Element of G such that
A2: X = ((1). G) * g by A1, Def16;
 x = {g} by A2, Th110;
hence  x in  {  {a} where a is Element of G : verum  }  ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  {a} where a is Element of G : verum  }  or x in Right_Cosets ((1). G) )
assume  x in  {  {a} where a is Element of G : verum  }  ; ::_thesis: x in Right_Cosets ((1). G)
then consider a being Element of G such that
A3: x = {a} ;
 ((1). G) * a = {a} by Th110;
hence  x in Right_Cosets ((1). G) by A3, Def16; ::_thesis: verum
end;

theorem :: GROUP_2:140
for G being Group
for H being strict Subgroup of G st Left_Cosets H =  {  {a} where a is Element of G : verum  }  holds
H = (1). G
proof
let G be Group; ::_thesis: for H being strict Subgroup of G st Left_Cosets H =  {  {a} where a is Element of G : verum  }  holds
H = (1). G
let H be strict Subgroup of G; ::_thesis: ( Left_Cosets H =  {  {a} where a is Element of G : verum  }  implies H = (1). G )
assume A1: Left_Cosets H =  {  {a} where a is Element of G : verum  }  ; ::_thesis: H = (1). G
A2: the carrier of H c= {(1_ G)}
proof
set a = the Element of G;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of H or x in {(1_ G)} )
assume  x in the carrier of H ; ::_thesis: x in {(1_ G)}
then reconsider h = x as Element of H ;
A3: h in H by STRUCT_0:def_5;
reconsider h = h as Element of G by Th42;
 the Element of G * H in Left_Cosets H by Def15;
then consider b being Element of G such that
A4: the Element of G * H = {b} by A1;
 the Element of G * h in the Element of G * H by A3, Th103;
then A5: the Element of G * h = b by A4, TARSKI:def_1;
 1_ G in H by Th46;
then  the Element of G * (1_ G) in the Element of G * H by Th103;
then  the Element of G * (1_ G) = b by A4, TARSKI:def_1;
then  h = 1_ G by A5, GROUP_1:6;
hence  x in {(1_ G)} by TARSKI:def_1; ::_thesis: verum
end;
 1_ G in H by Th46;
then  1_ G in the carrier of H by STRUCT_0:def_5;
then  {(1_ G)} c= the carrier of H by ZFMISC_1:31;
then  {(1_ G)} = the carrier of H by A2, XBOOLE_0:def_10;
hence  H = (1). G by Def7; ::_thesis: verum
end;

theorem :: GROUP_2:141
for G being Group
for H being strict Subgroup of G st Right_Cosets H =  {  {a} where a is Element of G : verum  }  holds
H = (1). G
proof
let G be Group; ::_thesis: for H being strict Subgroup of G st Right_Cosets H =  {  {a} where a is Element of G : verum  }  holds
H = (1). G
let H be strict Subgroup of G; ::_thesis: ( Right_Cosets H =  {  {a} where a is Element of G : verum  }  implies H = (1). G )
assume A1: Right_Cosets H =  {  {a} where a is Element of G : verum  }  ; ::_thesis: H = (1). G
A2: the carrier of H c= {(1_ G)}
proof
set a = the Element of G;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of H or x in {(1_ G)} )
assume  x in the carrier of H ; ::_thesis: x in {(1_ G)}
then reconsider h = x as Element of H ;
A3: h in H by STRUCT_0:def_5;
reconsider h = h as Element of G by Th42;
 H * the Element of G in Right_Cosets H by Def16;
then consider b being Element of G such that
A4: H * the Element of G = {b} by A1;
 h * the Element of G in H * the Element of G by A3, Th104;
then A5: h * the Element of G = b by A4, TARSKI:def_1;
 1_ G in H by Th46;
then  (1_ G) * the Element of G in H * the Element of G by Th104;
then  (1_ G) * the Element of G = b by A4, TARSKI:def_1;
then  h = 1_ G by A5, GROUP_1:6;
hence  x in {(1_ G)} by TARSKI:def_1; ::_thesis: verum
end;
 1_ G in H by Th46;
then  1_ G in the carrier of H by STRUCT_0:def_5;
then  {(1_ G)} c= the carrier of H by ZFMISC_1:31;
then  {(1_ G)} = the carrier of H by A2, XBOOLE_0:def_10;
hence  H = (1). G by Def7; ::_thesis: verum
end;

theorem Th142: :: GROUP_2:142
for G being Group holds
( Left_Cosets ((Omega). G) = { the carrier of G} & Right_Cosets ((Omega). G) = { the carrier of G} )
proof
let G be Group; ::_thesis: ( Left_Cosets ((Omega). G) = { the carrier of G} & Right_Cosets ((Omega). G) = { the carrier of G} )
set a = the Element of G;
A1: Left_Cosets ((Omega). G) c= { the carrier of G}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Left_Cosets ((Omega). G) or x in { the carrier of G} )
assume A2: x in Left_Cosets ((Omega). G) ; ::_thesis: x in { the carrier of G}
then reconsider X = x as Subset of G ;
consider a being Element of G such that
A3: X = a * ((Omega). G) by A2, Def15;
 a * ((Omega). G) = the carrier of G by Th111;
hence  x in { the carrier of G} by A3, TARSKI:def_1; ::_thesis: verum
end;
A4: Right_Cosets ((Omega). G) c= { the carrier of G}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Right_Cosets ((Omega). G) or x in { the carrier of G} )
assume A5: x in Right_Cosets ((Omega). G) ; ::_thesis: x in { the carrier of G}
then reconsider X = x as Subset of G ;
consider a being Element of G such that
A6: X = ((Omega). G) * a by A5, Def16;
 ((Omega). G) * a = the carrier of G by Th111;
hence  x in { the carrier of G} by A6, TARSKI:def_1; ::_thesis: verum
end;
 ((Omega). G) * the Element of G = the carrier of G by Th111;
then  the carrier of G in Right_Cosets ((Omega). G) by Def16;
then A7: { the carrier of G} c= Right_Cosets ((Omega). G) by ZFMISC_1:31;
 the Element of G * ((Omega). G) = the carrier of G by Th111;
then  the carrier of G in Left_Cosets ((Omega). G) by Def15;
then  { the carrier of G} c= Left_Cosets ((Omega). G) by ZFMISC_1:31;
hence  ( Left_Cosets ((Omega). G) = { the carrier of G} & Right_Cosets ((Omega). G) = { the carrier of G} ) by A7, A1, A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th143: :: GROUP_2:143
for G being strict Group
for H being strict Subgroup of G st Left_Cosets H = { the carrier of G} holds
H = G
proof
let G be strict Group; ::_thesis: for H being strict Subgroup of G st Left_Cosets H = { the carrier of G} holds
H = G
let H be strict Subgroup of G; ::_thesis: ( Left_Cosets H = { the carrier of G} implies H = G )
assume  Left_Cosets H = { the carrier of G} ; ::_thesis: H = G
then A1: the carrier of G in Left_Cosets H by TARSKI:def_1;
then reconsider T = the carrier of G as Subset of G ;
consider a being Element of G such that
A2: T = a * H by A1, Def15;
now__::_thesis:_for_g_being_Element_of_G_holds_g_in_H
let g be Element of G; ::_thesis: g in H
 ex b being Element of G st
( a * g = a * b & b in H ) by A2, Th103;
hence  g in H by GROUP_1:6; ::_thesis: verum
end;
hence  H = G by Th62; ::_thesis: verum
end;

theorem :: GROUP_2:144
for G being strict Group
for H being strict Subgroup of G st Right_Cosets H = { the carrier of G} holds
H = G
proof
let G be strict Group; ::_thesis: for H being strict Subgroup of G st Right_Cosets H = { the carrier of G} holds
H = G
let H be strict Subgroup of G; ::_thesis: ( Right_Cosets H = { the carrier of G} implies H = G )
assume  Right_Cosets H = { the carrier of G} ; ::_thesis: H = G
then A1: the carrier of G in Right_Cosets H by TARSKI:def_1;
then reconsider T = the carrier of G as Subset of G ;
consider a being Element of G such that
A2: T = H * a by A1, Def16;
now__::_thesis:_for_g_being_Element_of_G_holds_g_in_H
let g be Element of G; ::_thesis: g in H
 ex b being Element of G st
( g * a = b * a & b in H ) by A2, Th104;
hence  g in H by GROUP_1:6; ::_thesis: verum
end;
hence  H = G by Th62; ::_thesis: verum
end;

definition
let G be Group;
let H be Subgroup of G;
func Index H ->  Cardinal equals :: GROUP_2:def 17
 card (Left_Cosets H);
correctness
coherence
card (Left_Cosets H) is Cardinal;
;
end;

:: deftheorem  defines Index GROUP_2:def_17_:_
 for G being Group
for H being Subgroup of G holds Index H = card (Left_Cosets H);

theorem :: GROUP_2:145
for G being Group
for H being Subgroup of G holds
( Index H = card (Left_Cosets H) & Index H = card (Right_Cosets H) )
proof
let G be Group; ::_thesis: for H being Subgroup of G holds
( Index H = card (Left_Cosets H) & Index H = card (Right_Cosets H) )
let H be Subgroup of G; ::_thesis: ( Index H = card (Left_Cosets H) & Index H = card (Right_Cosets H) )
thus  Index H = card (Left_Cosets H) ; ::_thesis: Index H = card (Right_Cosets H)
 Left_Cosets H, Right_Cosets H are_equipotent by Th136;
hence  Index H = card (Right_Cosets H) by CARD_1:5; ::_thesis: verum
end;

definition
let G be Group;
let H be Subgroup of G;
assume A1: Left_Cosets H is finite ;
func index H ->  Element of NAT  means :Def18: :: GROUP_2:def 18
 ex B being finite set st
( B = Left_Cosets H & it = card B );
existence
 ex b1 being Element of NAT ex B being finite set st
( B = Left_Cosets H & b1 = card B )
proof
reconsider B = Left_Cosets H as finite set by A1;
take  card B ; ::_thesis: ex B being finite set st
( B = Left_Cosets H & card B = card B )
take  B ; ::_thesis: ( B = Left_Cosets H & card B = card B )
thus  ( B = Left_Cosets H & card B = card B ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT st ex B being finite set st
( B = Left_Cosets H & b1 = card B ) & ex B being finite set st
( B = Left_Cosets H & b2 = card B ) holds
b1 = b2 ;
end;

:: deftheorem Def18 defines index GROUP_2:def_18_:_
 for G being Group
for H being Subgroup of G st Left_Cosets H is finite holds
for b3 being Element of NAT holds
( b3 = index H iff ex B being finite set st
( B = Left_Cosets H & b3 = card B ) );

theorem :: GROUP_2:146
for G being Group
for H being Subgroup of G st Left_Cosets H is finite holds
( ex B being finite set st
( B = Left_Cosets H & index H = card B ) & ex C being finite set st
( C = Right_Cosets H & index H = card C ) )
proof
let G be Group; ::_thesis: for H being Subgroup of G st Left_Cosets H is finite holds
( ex B being finite set st
( B = Left_Cosets H & index H = card B ) & ex C being finite set st
( C = Right_Cosets H & index H = card C ) )
let H be Subgroup of G; ::_thesis: ( Left_Cosets H is finite implies ( ex B being finite set st
( B = Left_Cosets H & index H = card B ) & ex C being finite set st
( C = Right_Cosets H & index H = card C ) ) )
assume  Left_Cosets H is finite ; ::_thesis: ( ex B being finite set st
( B = Left_Cosets H & index H = card B ) & ex C being finite set st
( C = Right_Cosets H & index H = card C ) )
then reconsider B = Left_Cosets H as finite set ;
hereby  ::_thesis: ex C being finite set st
( C = Right_Cosets H & index H = card C )
take B = B; ::_thesis: ( B = Left_Cosets H & index H = card B )
thus  ( B = Left_Cosets H & index H = card B ) by Def18; ::_thesis: verum
end;
then reconsider C = Right_Cosets H as finite set by Th136, CARD_1:38;
take  C ; ::_thesis: ( C = Right_Cosets H & index H = card C )
 ( index H = card B & B,C are_equipotent ) by Def18, Th136;
hence  ( C = Right_Cosets H & index H = card C ) by CARD_1:5; ::_thesis: verum
end;

Lm5:  for k being Nat
for X being finite set st ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) holds
ex C being finite set st
( C = union X & card C = k * (card X) )
proof
let k be Nat; ::_thesis: for X being finite set st ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) holds
ex C being finite set st
( C = union X & card C = k * (card X) )
let X be finite set ; ::_thesis: ( ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st
( C = union X & card C = k * (card X) ) )
percases ( X = {} or X <> {} ) ;
supposeA1: X = {} ; ::_thesis: ( ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st
( C = union X & card C = k * (card X) ) )
reconsider E = {} as finite set ;
assume  for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ; ::_thesis: ex C being finite set st
( C = union X & card C = k * (card X) )
take  E ; ::_thesis: ( E = union X & card E = k * (card X) )
thus  ( E = union X & card E = k * (card X) ) by A1, CARD_1:27, ZFMISC_1:2; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: ( ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st
( C = union X & card C = k * (card X) ) )
then reconsider D = X as non empty set ;
defpred S1[ Element of Fin D] means ( ( for Y being set st Y in $1 holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in $1 & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st
( C = union $1 & card C = k * (card $1) ) );
A2: for S being Element of Fin D
for s being Element of D st S1[S] & not s in S holds
S1[S \/ {.s.}]
proof
let S be Element of Fin D; ::_thesis: for s being Element of D st S1[S] & not s in S holds
S1[S \/ {.s.}]
let s be Element of D; ::_thesis: ( S1[S] & not s in S implies S1[S \/ {.s.}] )
assume that
A3: ( ( for Y being set st Y in S holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st
( C = union S & card C = k * (card S) ) ) and
A4: not s in S and
A5: for Y being set st Y in S \/ {s} holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ; ::_thesis: ex C being finite set st
( C = union (S \/ {.s.}) & card C = k * (card (S \/ {.s.})) )
A6: card (S \/ {s}) = (card S) + 1 by A4, CARD_2:41;
now__::_thesis:_for_Y_being_set_st_Y_in_S_holds_
Y_is_finite
let Y be set ; ::_thesis: ( Y in S implies Y is finite )
assume  Y in S ; ::_thesis: Y is finite
then  Y in S \/ {s} by XBOOLE_0:def_3;
then  ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) by A5;
hence  Y is finite ; ::_thesis: verum
end;
then reconsider D1 = union S as finite set by FINSET_1:7;
A7: now__::_thesis:_for_Y,_Z_being_set_st_Y_in_S_holds_
ex_B_being_finite_set_st_
(_B_=_Y_&_card_B_=_k_&_(_for_Z_being_set_st_Z_in_S_&_Y_<>_Z_holds_
(_Y,Z_are_equipotent_&_Y_misses_Z_)_)_)
let Y, Z be set ; ::_thesis: ( Y in S implies ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) )
assume  Y in S ; ::_thesis: ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) )
then  Y in S \/ {s} by XBOOLE_0:def_3;
then consider B being finite set  such that
A8: ( B = Y & card B = k ) and
A9: for Z being set st Z in S \/ {s} & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) by A5;
take B = B; ::_thesis: ( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) )
thus  ( B = Y & card B = k ) by A8; ::_thesis: for Z being set st Z in S & Y <> Z holds
( Y,Z are_equipotent & Y misses Z )
let Z be set ; ::_thesis: ( Z in S & Y <> Z implies ( Y,Z are_equipotent & Y misses Z ) )
assume that
A10: Z in S and
A11: Y <> Z ; ::_thesis: ( Y,Z are_equipotent & Y misses Z )
 Z in S \/ {s} by A10, XBOOLE_0:def_3;
hence  ( Y,Z are_equipotent & Y misses Z ) by A9, A11; ::_thesis: verum
end;
 s in {s} by TARSKI:def_1;
then  s in S \/ {s} by XBOOLE_0:def_3;
then A12: ex B being finite set st
( B = s & card B = k & ( for Z being set st Z in S \/ {s} & s <> Z holds
( s,Z are_equipotent & s misses Z ) ) ) by A5;
then reconsider T = s as finite set ;
A13: union {s} = s by ZFMISC_1:25;
then A14: union (S \/ {s}) = D1 \/ T by ZFMISC_1:78;
then reconsider D2 = union (S \/ {s}) as finite set ;
take  D2 ; ::_thesis: ( D2 = union (S \/ {.s.}) & card D2 = k * (card (S \/ {.s.})) )
thus  D2 = union (S \/ {s}) ; ::_thesis: card D2 = k * (card (S \/ {.s.}))
now__::_thesis:_not_union_S_meets_union_{s}
assume  union S meets union {s} ; ::_thesis: contradiction
then consider x being set  such that
A15: x in union S and
A16: x in union {s} by XBOOLE_0:3;
consider Y being set  such that
A17: x in Y and
A18: Y in S by A15, TARSKI:def_4;
consider Z being set  such that
A19: x in Z and
A20: Z in {s} by A16, TARSKI:def_4;
A21: Z in S \/ {s} by A20, XBOOLE_0:def_3;
 Y in S \/ {s} by A18, XBOOLE_0:def_3;
then A22: ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) by A5;
 Z <> Y by A4, A18, A20, TARSKI:def_1;
then  Y misses Z by A21, A22;
hence  contradiction by A17, A19, XBOOLE_0:3; ::_thesis: verum
end;
hence  card D2 = (k * (card S)) + (k * 1) by A3, A13, A12, A14, A7, CARD_2:40
.= k * (card (S \/ {s})) by A6 ;
::_thesis: verum
end;
A23: X is Element of Fin D by FINSUB_1:def_5;
A24: S1[ {}. D] by ZFMISC_1:2;
 for B being Element of Fin D holds S1[B] from SETWISEO:sch_2(A24, A2);
hence  ( ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st
( C = union X & card C = k * (card X) ) ) by A23; ::_thesis: verum
end;
end;
end;

theorem Th147: :: GROUP_2:147
for G being finite Group
for H being Subgroup of G holds card G = (card H) * (index H)
proof
let G be finite Group; ::_thesis: for H being Subgroup of G holds card G = (card H) * (index H)
let H be Subgroup of G; ::_thesis: card G = (card H) * (index H)
reconsider C = Left_Cosets H as finite set ;
now__::_thesis:_for_X_being_set_st_X_in_C_holds_
ex_B_being_finite_set_st_
(_B_=_X_&_card_B_=_card_H_&_(_for_Y_being_set_st_Y_in_C_&_X_<>_Y_holds_
(_X,Y_are_equipotent_&_X_misses_Y_)_)_)
let X be set ; ::_thesis: ( X in C implies ex B being finite set st
( B = X & card B = card H & ( for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y ) ) ) )
assume A1: X in C ; ::_thesis: ex B being finite set st
( B = X & card B = card H & ( for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y ) ) )
then reconsider x = X as Subset of G ;
 x is finite ;
then reconsider B = X as finite set ;
take B = B; ::_thesis: ( B = X & card B = card H & ( for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y ) ) )
thus  B = X ; ::_thesis: ( card B = card H & ( for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y ) ) )
consider a being Element of G such that
A2: x = a * H by A1, Def15;
 ex B, C being finite set st
( B = a * H & C = H * a & card H = card B & card H = card C ) by Th133;
hence  card B = card H by A2; ::_thesis: for Y being set st Y in C & X <> Y holds
( X,Y are_equipotent & X misses Y )
let Y be set ; ::_thesis: ( Y in C & X <> Y implies ( X,Y are_equipotent & X misses Y ) )
assume that
A3: Y in C and
A4: X <> Y ; ::_thesis: ( X,Y are_equipotent & X misses Y )
reconsider y = Y as Subset of G by A3;
A5: ex b being Element of G st y = b * H by A3, Def15;
hence  X,Y are_equipotent by A2, Th128; ::_thesis: X misses Y
thus  X misses Y by A2, A4, A5, Th115; ::_thesis: verum
end;
then A6: ex D being finite set st
( D = union C & card D = (card H) * (card C) ) by Lm5;
 union (Left_Cosets H) = the carrier of G by Th137;
hence  card G = (card H) * (index H) by A6, Def18; ::_thesis: verum
end;

theorem :: GROUP_2:148
for G being finite Group
for H being Subgroup of G holds card H divides card G
proof
let G be finite Group; ::_thesis: for H being Subgroup of G holds card H divides card G
let H be Subgroup of G; ::_thesis: card H divides card G
 card G = (card H) * (index H) by Th147;
hence  card H divides card G by NAT_D:def_3; ::_thesis: verum
end;

theorem :: GROUP_2:149
for G being finite Group
for I, H being Subgroup of G
for J being Subgroup of H st I = J holds
index I = (index J) * (index H)
proof
let G be finite Group; ::_thesis: for I, H being Subgroup of G
for J being Subgroup of H st I = J holds
index I = (index J) * (index H)
let I, H be Subgroup of G; ::_thesis: for J being Subgroup of H st I = J holds
index I = (index J) * (index H)
let J be Subgroup of H; ::_thesis: ( I = J implies index I = (index J) * (index H) )
assume A1: I = J ; ::_thesis: index I = (index J) * (index H)
 ( card G = (card H) * (index H) & card H = (card J) * (index J) ) by Th147;
then  (card I) * ((index J) * (index H)) = (card I) * (index I) by A1, Th147;
hence  index I = (index J) * (index H) by XCMPLX_1:5; ::_thesis: verum
end;

theorem :: GROUP_2:150
for G being Group holds index ((Omega). G) = 1
proof
let G be Group; ::_thesis: index ((Omega). G) = 1
 Left_Cosets ((Omega). G) = { the carrier of G} by Th142;
hence  index ((Omega). G) = card { the carrier of G} by Def18
.= 1 by CARD_1:30 ;
::_thesis: verum
end;

theorem :: GROUP_2:151
for G being strict Group
for H being strict Subgroup of G st Left_Cosets H is finite & index H = 1 holds
H = G
proof
let G be strict Group; ::_thesis: for H being strict Subgroup of G st Left_Cosets H is finite & index H = 1 holds
H = G
let H be strict Subgroup of G; ::_thesis: ( Left_Cosets H is finite & index H = 1 implies H = G )
assume that
A1: Left_Cosets H is finite and
A2: index H = 1 ; ::_thesis: H = G
reconsider B = Left_Cosets H as finite set by A1;
 card B = 1 by A2, Def18;
then consider x being set  such that
A3: Left_Cosets H = {x} by CARD_2:42;
 ( union {x} = x & union (Left_Cosets H) = the carrier of G ) by Th137, ZFMISC_1:25;
hence  H = G by A3, Th143; ::_thesis: verum
end;

theorem :: GROUP_2:152
for G being Group holds Index ((1). G) = card G
proof
let G be Group; ::_thesis: Index ((1). G) = card G
deffunc H1( set ) ->  set = {$1};
consider f being Function such that
A1: dom f = the carrier of G and
A2: for x being set st x in the carrier of G holds
f . x = H1(x) from FUNCT_1:sch_3();
A3: rng f = Left_Cosets ((1). G)
proof
thus  rng f c= Left_Cosets ((1). G) :: according to XBOOLE_0:def_10 ::_thesis: Left_Cosets ((1). G) c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Left_Cosets ((1). G) )
assume  x in rng f ; ::_thesis: x in Left_Cosets ((1). G)
then consider y being set  such that
A4: y in dom f and
A5: f . y = x by FUNCT_1:def_3;
reconsider y = y as Element of G by A1, A4;
 x = {y} by A2, A5;
then  x in  {  {a} where a is Element of G : verum  }  ;
hence  x in Left_Cosets ((1). G) by Th138; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Left_Cosets ((1). G) or x in rng f )
assume  x in Left_Cosets ((1). G) ; ::_thesis: x in rng f
then  x in  {  {a} where a is Element of G : verum  }  by Th138;
then consider a being Element of G such that
A6: x = {a} ;
 f . a = {a} by A2;
hence  x in rng f by A1, A6, FUNCT_1:def_3; ::_thesis: verum
end;
 f is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A7: ( x in dom f & y in dom f ) and
A8: f . x = f . y ; ::_thesis: x = y
 ( f . y = {y} & f . x = {x} ) by A1, A2, A7;
hence  x = y by A8, ZFMISC_1:3; ::_thesis: verum
end;
then  the carrier of G, Left_Cosets ((1). G) are_equipotent by A1, A3, WELLORD2:def_4;
hence  Index ((1). G) = card G by CARD_1:5; ::_thesis: verum
end;

theorem :: GROUP_2:153
for G being finite Group holds index ((1). G) = card G
proof
let G be finite Group; ::_thesis: index ((1). G) = card G
thus  card G = (card ((1). G)) * (index ((1). G)) by Th147
.= 1 * (index ((1). G)) by Th69
.= index ((1). G) ; ::_thesis: verum
end;

theorem Th154: :: GROUP_2:154
for G being finite Group
for H being strict Subgroup of G st index H = card G holds
H = (1). G
proof
let G be finite Group; ::_thesis: for H being strict Subgroup of G st index H = card G holds
H = (1). G
let H be strict Subgroup of G; ::_thesis: ( index H = card G implies H = (1). G )
assume  index H = card G ; ::_thesis: H = (1). G
then  1 * (card G) = (card H) * (card G) by Th147;
hence  H = (1). G by Th70, XCMPLX_1:5; ::_thesis: verum
end;

theorem :: GROUP_2:155
for G being Group
for H being strict Subgroup of G st Left_Cosets H is finite & Index H = card G holds
( G is finite & H = (1). G )
proof
let G be Group; ::_thesis: for H being strict Subgroup of G st Left_Cosets H is finite & Index H = card G holds
( G is finite & H = (1). G )
let H be strict Subgroup of G; ::_thesis: ( Left_Cosets H is finite & Index H = card G implies ( G is finite & H = (1). G ) )
assume that
A1: Left_Cosets H is finite and
A2: Index H = card G ; ::_thesis: ( G is finite & H = (1). G )
thus A3: G is finite by A1, A2; ::_thesis: H = (1). G
 ex B being finite set st
( B = Left_Cosets H & index H = card B ) by A1, Def18;
hence  H = (1). G by A2, A3, Th154; ::_thesis: verum
end;

theorem :: GROUP_2:156
for k being Nat
for X being finite set st ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) holds
ex C being finite set st
( C = union X & card C = k * (card X) ) by Lm5;