:: GROUP_4 semantic presentation

begin

definition
let D be non empty set ;
let F be FinSequence of D;
let X be set ;
:: original: -
redefine funcF - X ->  FinSequence of D;
coherence
 F - X is FinSequence of D by FINSEQ_3:86;
end;

scheme :: GROUP_4:sch 1
MeetSbgEx{ F1() ->  Group, P1[ set ] } :
 ex H being strict Subgroup of F1() st the carrier of H = meet  {  A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] )  }
provided
A1: ex H being strict Subgroup of F1() st P1[H]
proof
set X =  {  A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] )  }  ;
consider T being strict Subgroup of F1() such that
A2: P1[T] by A1;
A3: carr T in  {  A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] )  }  by A2;
then reconsider Y = meet  {  A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] )  }  as Subset of F1() by SETFAM_1:7;
A4: now__::_thesis:_for_a_being_Element_of_F1()_st_a_in_Y_holds_
a_"_in_Y
let a be Element of F1(); ::_thesis: ( a in Y implies a " in Y )
assume A5: a in Y ; ::_thesis: a " in Y
now__::_thesis:_for_Z_being_set_st_Z_in__{__A_where_A_is_Subset_of_F1()_:_ex_K_being_strict_Subgroup_of_F1()_st_
(_A_=_the_carrier_of_K_&_P1[K]_)__}__holds_
a_"_in_Z
let Z be set ; ::_thesis: ( Z in  {  A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] )  }  implies a " in Z )
assume A6: Z in  {  A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] )  }  ; ::_thesis: a " in Z
then consider A being Subset of F1() such that
A7: A = Z and
A8: ex H being strict Subgroup of F1() st
( A = the carrier of H & P1[H] ) ;
consider H being Subgroup of F1() such that
A9: A = the carrier of H and
 P1[H] by A8;
 a in the carrier of H by A5, A6, A7, A9, SETFAM_1:def_1;
then  a in H by STRUCT_0:def_5;
then  a " in H by GROUP_2:51;
hence  a " in Z by A7, A9, STRUCT_0:def_5; ::_thesis: verum
end;
hence  a " in Y by A3, SETFAM_1:def_1; ::_thesis: verum
end;
A10: now__::_thesis:_for_a,_b_being_Element_of_F1()_st_a_in_Y_&_b_in_Y_holds_
a_*_b_in_Y
let a, b be Element of F1(); ::_thesis: ( a in Y & b in Y implies a * b in Y )
assume that
A11: a in Y and
A12: b in Y ; ::_thesis: a * b in Y
now__::_thesis:_for_Z_being_set_st_Z_in__{__A_where_A_is_Subset_of_F1()_:_ex_K_being_strict_Subgroup_of_F1()_st_
(_A_=_the_carrier_of_K_&_P1[K]_)__}__holds_
a_*_b_in_Z
let Z be set ; ::_thesis: ( Z in  {  A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] )  }  implies a * b in Z )
assume A13: Z in  {  A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] )  }  ; ::_thesis: a * b in Z
then consider A being Subset of F1() such that
A14: A = Z and
A15: ex H being strict Subgroup of F1() st
( A = the carrier of H & P1[H] ) ;
consider H being Subgroup of F1() such that
A16: A = the carrier of H and
 P1[H] by A15;
 b in the carrier of H by A12, A13, A14, A16, SETFAM_1:def_1;
then A17: b in H by STRUCT_0:def_5;
 a in the carrier of H by A11, A13, A14, A16, SETFAM_1:def_1;
then  a in H by STRUCT_0:def_5;
then  a * b in H by A17, GROUP_2:50;
hence  a * b in Z by A14, A16, STRUCT_0:def_5; ::_thesis: verum
end;
hence  a * b in Y by A3, SETFAM_1:def_1; ::_thesis: verum
end;
now__::_thesis:_for_Z_being_set_st_Z_in__{__A_where_A_is_Subset_of_F1()_:_ex_K_being_strict_Subgroup_of_F1()_st_
(_A_=_the_carrier_of_K_&_P1[K]_)__}__holds_
1__F1()_in_Z
let Z be set ; ::_thesis: ( Z in  {  A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] )  }  implies 1_ F1() in Z )
assume  Z in  {  A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] )  }  ; ::_thesis: 1_ F1() in Z
then consider A being Subset of F1() such that
A18: Z = A and
A19: ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) ;
consider H being Subgroup of F1() such that
A20: A = the carrier of H and
 P1[H] by A19;
 1_ F1() in H by GROUP_2:46;
hence  1_ F1() in Z by A18, A20, STRUCT_0:def_5; ::_thesis: verum
end;
then  Y <> {} by A3, SETFAM_1:def_1;
hence  ex H being strict Subgroup of F1() st the carrier of H = meet  {  A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] )  }  by A10, A4, GROUP_2:52; ::_thesis: verum
end;


scheme :: GROUP_4:sch 2
SubgrSep{ F1() ->  Group, P1[ set ] } :
 ex X being set st
( X c= Subgroups F1() & ( for H being strict Subgroup of F1() holds
( H in X iff P1[H] ) ) )
proof
defpred S1[ set ] means  ex H being Subgroup of F1() st
( $1 = H & P1[H] );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in Subgroups F1() & S1[x] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: ( X c= Subgroups F1() & ( for H being strict Subgroup of F1() holds
( H in X iff P1[H] ) ) )
thus  X c= Subgroups F1() ::_thesis: for H being strict Subgroup of F1() holds
( H in X iff P1[H] )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Subgroups F1() )
assume  x in X ; ::_thesis: x in Subgroups F1()
hence  x in Subgroups F1() by A1; ::_thesis: verum
end;
let H be strict Subgroup of F1(); ::_thesis: ( H in X iff P1[H] )
thus  ( H in X implies P1[H] ) ::_thesis: ( P1[H] implies H in X )
proof
assume  H in X ; ::_thesis: P1[H]
then  ex H1 being Subgroup of F1() st
( H = H1 & P1[H1] ) by A1;
hence  P1[H] ; ::_thesis: verum
end;
A2: H in Subgroups F1() by GROUP_3:def_1;
assume  P1[H] ; ::_thesis: H in X
hence  H in X by A1, A2; ::_thesis: verum
end;

definition
let i be Integer;
func @ i ->  Element of INT  equals :: GROUP_4:def 1
i;
coherence
 i is Element of INT by INT_1:def_2;
end;

:: deftheorem  defines @ GROUP_4:def_1_:_
 for i being Integer holds @ i = i;

theorem Th1: :: GROUP_4:1
for n being Element of NAT
for G being Group
for a being Element of G
for H being Subgroup of G
for h being Element of H st a = h holds
a |^ n = h |^ n
proof
let n be Element of NAT ; ::_thesis: for G being Group
for a being Element of G
for H being Subgroup of G
for h being Element of H st a = h holds
a |^ n = h |^ n
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G
for h being Element of H st a = h holds
a |^ n = h |^ n
let a be Element of G; ::_thesis: for H being Subgroup of G
for h being Element of H st a = h holds
a |^ n = h |^ n
let H be Subgroup of G; ::_thesis: for h being Element of H st a = h holds
a |^ n = h |^ n
let h be Element of H; ::_thesis: ( a = h implies a |^ n = h |^ n )
defpred S1[ Element of NAT ] means a |^ $1 = h |^ $1;
assume A1: a = h ; ::_thesis: a |^ n = h |^ n
A2: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; ::_thesis: S1[n + 1]
a |^ (n + 1) = (a |^ n) * a by GROUP_1:34
.= (h |^ n) * h by A1, A3, GROUP_2:43
.= h |^ (n + 1) by GROUP_1:34 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
a |^ 0 = 1_ G by GROUP_1:25
.= 1_ H by GROUP_2:44
.= h |^ 0 by GROUP_1:25 ;
then A4: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2);
hence  a |^ n = h |^ n ; ::_thesis: verum
end;

theorem :: GROUP_4:2
for i being Integer
for G being Group
for a being Element of G
for H being Subgroup of G
for h being Element of H st a = h holds
a |^ i = h |^ i
proof
let i be Integer; ::_thesis: for G being Group
for a being Element of G
for H being Subgroup of G
for h being Element of H st a = h holds
a |^ i = h |^ i
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G
for h being Element of H st a = h holds
a |^ i = h |^ i
let a be Element of G; ::_thesis: for H being Subgroup of G
for h being Element of H st a = h holds
a |^ i = h |^ i
let H be Subgroup of G; ::_thesis: for h being Element of H st a = h holds
a |^ i = h |^ i
let h be Element of H; ::_thesis: ( a = h implies a |^ i = h |^ i )
assume A1: a = h ; ::_thesis: a |^ i = h |^ i
now__::_thesis:_a_|^_i_=_h_|^_i
percases ( i >= 0 or i < 0 ) ;
supposeA2: i >= 0 ; ::_thesis: a |^ i = h |^ i
hence a |^ i = a |^ (abs i) by ABSVALUE:def_1
.= h |^ (abs i) by A1, Th1
.= h |^ i by A2, ABSVALUE:def_1 ;
::_thesis: verum
end;
supposeA3: i < 0 ; ::_thesis: a |^ i = h |^ i
A4: a |^ (abs i) = h |^ (abs i) by A1, Th1;
thus a |^ i = (a |^ (abs i)) " by A3, GROUP_1:30
.= (h |^ (abs i)) " by A4, GROUP_2:48
.= h |^ i by A3, GROUP_1:30 ; ::_thesis: verum
end;
end;
end;
hence  a |^ i = h |^ i ; ::_thesis: verum
end;

theorem Th3: :: GROUP_4:3
for n being Element of NAT
for G being Group
for a being Element of G
for H being Subgroup of G st a in H holds
a |^ n in H
proof
let n be Element of NAT ; ::_thesis: for G being Group
for a being Element of G
for H being Subgroup of G st a in H holds
a |^ n in H
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G st a in H holds
a |^ n in H
let a be Element of G; ::_thesis: for H being Subgroup of G st a in H holds
a |^ n in H
let H be Subgroup of G; ::_thesis: ( a in H implies a |^ n in H )
defpred S1[ Element of NAT ] means a |^ $1 in H;
assume A1: a in H ; ::_thesis: a |^ n in H
A2: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
A3: a |^ (n + 1) = (a |^ n) * a by GROUP_1:34;
assume  S1[n] ; ::_thesis: S1[n + 1]
hence  S1[n + 1] by A1, A3, GROUP_2:50; ::_thesis: verum
end;
 a |^ 0 = 1_ G by GROUP_1:25;
then A4: S1[ 0 ] by GROUP_2:46;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2);
hence  a |^ n in H ; ::_thesis: verum
end;

theorem Th4: :: GROUP_4:4
for i being Integer
for G being Group
for a being Element of G
for H being Subgroup of G st a in H holds
a |^ i in H
proof
let i be Integer; ::_thesis: for G being Group
for a being Element of G
for H being Subgroup of G st a in H holds
a |^ i in H
let G be Group; ::_thesis: for a being Element of G
for H being Subgroup of G st a in H holds
a |^ i in H
let a be Element of G; ::_thesis: for H being Subgroup of G st a in H holds
a |^ i in H
let H be Subgroup of G; ::_thesis: ( a in H implies a |^ i in H )
assume A1: a in H ; ::_thesis: a |^ i in H
now__::_thesis:_a_|^_i_in_H
percases ( i >= 0 or i < 0 ) ;
suppose i >= 0 ; ::_thesis: a |^ i in H
then  a |^ i = a |^ (abs i) by ABSVALUE:def_1;
hence  a |^ i in H by A1, Th3; ::_thesis: verum
end;
suppose i < 0 ; ::_thesis: a |^ i in H
then A2: a |^ i = (a |^ (abs i)) " by GROUP_1:30;
 a |^ (abs i) in H by A1, Th3;
hence  a |^ i in H by A2, GROUP_2:51; ::_thesis: verum
end;
end;
end;
hence  a |^ i in H ; ::_thesis: verum
end;

definition
let G be non empty multMagma ;
let F be FinSequence of the carrier of G;
func Product F ->  Element of G equals :: GROUP_4:def 2
 the multF of G "**" F;
correctness
coherence
the multF of G "**" F is Element of G;
;
end;

:: deftheorem  defines Product GROUP_4:def_2_:_
 for G being non empty multMagma
for F being FinSequence of the carrier of G holds Product F = the multF of G "**" F;

theorem :: GROUP_4:5
for G being non empty unital associative multMagma
for F1, F2 being FinSequence of the carrier of G holds Product (F1 ^ F2) = (Product F1) * (Product F2) by FINSOP_1:5;

theorem :: GROUP_4:6
for G being non empty unital multMagma
for F being FinSequence of the carrier of G
for a being Element of G holds Product (F ^ <*a*>) = (Product F) * a by FINSOP_1:4;

theorem :: GROUP_4:7
for G being non empty unital associative multMagma
for F being FinSequence of the carrier of G
for a being Element of G holds Product (<*a*> ^ F) = a * (Product F) by FINSOP_1:6;

theorem Th8: :: GROUP_4:8
for G being non empty unital multMagma holds Product (<*> the carrier of G) = 1_ G
proof
let G be non empty unital multMagma ; ::_thesis: Product (<*> the carrier of G) = 1_ G
set g = the multF of G;
 ( len (<*> the carrier of G) = 0 & the multF of G is having_a_unity ) ;
hence  Product (<*> the carrier of G) = the_unity_wrt the multF of G by FINSOP_1:def_1
.= 1_ G by GROUP_1:22 ;
::_thesis: verum
end;

theorem :: GROUP_4:9
for G being non empty multMagma
for a being Element of G holds Product <*a*> = a by FINSOP_1:11;

theorem :: GROUP_4:10
for G being non empty multMagma
for a, b being Element of G holds Product <*a,b*> = a * b by FINSOP_1:12;

theorem :: GROUP_4:11
for G being Group
for a, b, c being Element of G holds
( Product <*a,b,c*> = (a * b) * c & Product <*a,b,c*> = a * (b * c) )
proof
let G be Group; ::_thesis: for a, b, c being Element of G holds
( Product <*a,b,c*> = (a * b) * c & Product <*a,b,c*> = a * (b * c) )
let a, b, c be Element of G; ::_thesis: ( Product <*a,b,c*> = (a * b) * c & Product <*a,b,c*> = a * (b * c) )
A1: ( Product <*a*> = a & Product <*c*> = c ) by FINSOP_1:11;
A2: ( Product <*a,b*> = a * b & Product <*b,c*> = b * c ) by FINSOP_1:12;
 ( <*a,b,c*> = <*a*> ^ <*b,c*> & <*a,b,c*> = <*a,b*> ^ <*c*> ) by FINSEQ_1:43;
hence  ( Product <*a,b,c*> = (a * b) * c & Product <*a,b,c*> = a * (b * c) ) by A1, A2, FINSOP_1:5; ::_thesis: verum
end;

Lm1: now__::_thesis:_for_G_being_Group
for_a_being_Element_of_G_holds_Product_(0_|->_a)_=_a_|^_0
let G be Group; ::_thesis: for a being Element of G holds Product (0 |-> a) = a |^ 0
let a be Element of G; ::_thesis: Product (0 |-> a) = a |^ 0
thus  Product (0 |-> a) = Product (<*> the carrier of G)
.= 1_ G by Th8
.= a |^ 0 by GROUP_1:25 ; ::_thesis: verum
end;

Lm2: now__::_thesis:_for_G_being_Group
for_a_being_Element_of_G
for_n_being_Element_of_NAT_st_Product_(n_|->_a)_=_a_|^_n_holds_
Product_((n_+_1)_|->_a)_=_a_|^_(n_+_1)
let G be Group; ::_thesis: for a being Element of G
for n being Element of NAT st Product (n |-> a) = a |^ n holds
Product ((n + 1) |-> a) = a |^ (n + 1)
let a be Element of G; ::_thesis: for n being Element of NAT st Product (n |-> a) = a |^ n holds
Product ((n + 1) |-> a) = a |^ (n + 1)
let n be Element of NAT ; ::_thesis: ( Product (n |-> a) = a |^ n implies Product ((n + 1) |-> a) = a |^ (n + 1) )
assume A1: Product (n |-> a) = a |^ n ; ::_thesis: Product ((n + 1) |-> a) = a |^ (n + 1)
thus  Product ((n + 1) |-> a) = Product ((n |-> a) ^ <*a*>) by FINSEQ_2:60
.= (Product (n |-> a)) * (Product <*a*>) by FINSOP_1:5
.= (a |^ n) * a by A1, FINSOP_1:11
.= a |^ (n + 1) by GROUP_1:34 ; ::_thesis: verum
end;

theorem :: GROUP_4:12
for n being Element of NAT
for G being Group
for a being Element of G holds Product (n |-> a) = a |^ n
proof
let n be Element of NAT ; ::_thesis: for G being Group
for a being Element of G holds Product (n |-> a) = a |^ n
let G be Group; ::_thesis: for a being Element of G holds Product (n |-> a) = a |^ n
let a be Element of G; ::_thesis: Product (n |-> a) = a |^ n
defpred S1[ Element of NAT ] means  Product ($1 |-> a) = a |^ $1;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1] by Lm2;
A2: S1[ 0 ] by Lm1;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1);
hence  Product (n |-> a) = a |^ n ; ::_thesis: verum
end;

theorem :: GROUP_4:13
for G being Group
for F being FinSequence of the carrier of G holds Product (F - {(1_ G)}) = Product F
proof
let G be Group; ::_thesis: for F being FinSequence of the carrier of G holds Product (F - {(1_ G)}) = Product F
let F be FinSequence of the carrier of G; ::_thesis: Product (F - {(1_ G)}) = Product F
defpred S1[ FinSequence of the carrier of G] means  Product ($1 - {(1_ G)}) = Product $1;
A1: for F being FinSequence of the carrier of G
for a being Element of G st S1[F] holds
S1[F ^ <*a*>]
proof
let F be FinSequence of the carrier of G; ::_thesis: for a being Element of G st S1[F] holds
S1[F ^ <*a*>]
let a be Element of G; ::_thesis: ( S1[F] implies S1[F ^ <*a*>] )
assume A2: S1[F] ; ::_thesis: S1[F ^ <*a*>]
A3: Product ((F ^ <*a*>) - {(1_ G)}) = Product ((F - {(1_ G)}) ^ (<*a*> - {(1_ G)})) by FINSEQ_3:73
.= (Product F) * (Product (<*a*> - {(1_ G)})) by A2, FINSOP_1:5 ;
now__::_thesis:_S1[F_^_<*a*>]
percases ( a = 1_ G or a <> 1_ G ) ;
supposeA4: a = 1_ G ; ::_thesis: S1[F ^ <*a*>]
then  a in {(1_ G)} by TARSKI:def_1;
then  <*a*> - {(1_ G)} = <*> the carrier of G by FINSEQ_3:76;
then  Product (<*a*> - {(1_ G)}) = 1_ G by Th8;
hence  S1[F ^ <*a*>] by A3, A4, FINSOP_1:4; ::_thesis: verum
end;
suppose a <> 1_ G ; ::_thesis: S1[F ^ <*a*>]
then  not a in {(1_ G)} by TARSKI:def_1;
then  <*a*> - {(1_ G)} = <*a*> by FINSEQ_3:75;
hence  S1[F ^ <*a*>] by A3, FINSOP_1:5; ::_thesis: verum
end;
end;
end;
hence  S1[F ^ <*a*>] ; ::_thesis: verum
end;
A5: S1[ <*> the carrier of G] by FINSEQ_3:74;
 for F being FinSequence of the carrier of G holds S1[F] from FINSEQ_2:sch_2(A5, A1);
hence  Product (F - {(1_ G)}) = Product F ; ::_thesis: verum
end;

Lm3:  for F1 being FinSequence
for y being Element of NAT st y in dom F1 holds
( ((len F1) - y) + 1 is Element of NAT & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 )
proof
let F1 be FinSequence; ::_thesis: for y being Element of NAT st y in dom F1 holds
( ((len F1) - y) + 1 is Element of NAT & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 )
let y be Element of NAT ; ::_thesis: ( y in dom F1 implies ( ((len F1) - y) + 1 is Element of NAT & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 ) )
assume A1: y in dom F1 ; ::_thesis: ( ((len F1) - y) + 1 is Element of NAT & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 )
now__::_thesis:_not_((len_F1)_-_y)_+_1_<_0
assume  ((len F1) - y) + 1 < 0 ; ::_thesis: contradiction
then  1 < 0 - ((len F1) - y) by XREAL_1:20;
then  1 < y - (len F1) ;
then A2: (len F1) + 1 < y by XREAL_1:20;
 y <= len F1 by A1, FINSEQ_3:25;
hence  contradiction by A2, NAT_1:12; ::_thesis: verum
end;
then reconsider n = ((len F1) - y) + 1 as Element of NAT by INT_1:3;
 y >= 1 by A1, FINSEQ_3:25;
then  (n - 1) - y <= ((len F1) - y) - 1 by XREAL_1:13;
then A3: n - (y + 1) <= (len F1) - (y + 1) ;
 y + 0 <= len F1 by A1, FINSEQ_3:25;
then  ( 0 + 1 = 1 & 0 <= (len F1) - y ) by XREAL_1:19;
hence  ( ((len F1) - y) + 1 is Element of NAT & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 ) by A3, XREAL_1:6, XREAL_1:9; ::_thesis: verum
end;

theorem Th14: :: GROUP_4:14
for G being Group
for F1, F2 being FinSequence of the carrier of G st len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) holds
Product F1 = (Product F2) "
proof
let G be Group; ::_thesis: for F1, F2 being FinSequence of the carrier of G st len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) holds
Product F1 = (Product F2) "
let F1, F2 be FinSequence of the carrier of G; ::_thesis: ( len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " )
defpred S1[ Element of NAT ] means  for F1, F2 being FinSequence of the carrier of G st len F1 = $1 & len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) holds
Product F1 = (Product F2) " ;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
let F1, F2 be FinSequence of the carrier of G; ::_thesis: ( len F1 = n + 1 & len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " )
assume that
A3: len F1 = n + 1 and
A4: len F1 = len F2 and
A5: for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ; ::_thesis: Product F1 = (Product F2) "
reconsider p = F1 | (Seg n) as FinSequence of the carrier of G by FINSEQ_1:18;
deffunc H1( Nat) ->  set = F2 . ($1 + 1);
consider q being FinSequence such that
A6: len q = len p and
A7: for k being Nat st k in dom q holds
q . k = H1(k) from FINSEQ_1:sch_2();
A8: dom q = dom p by A6, FINSEQ_3:29;
A9: len p = n by A3, FINSEQ_3:53;
A10: rng q c= the carrier of G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng q or x in the carrier of G )
assume  x in rng q ; ::_thesis: x in the carrier of G
then consider y being set  such that
A11: y in dom q and
A12: x = q . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A11;
 y <= len p by A6, A11, FINSEQ_3:25;
then  ( 1 <= y + 1 & y + 1 <= len F2 ) by A3, A4, A9, NAT_1:12, XREAL_1:7;
then A13: y + 1 in dom F2 by FINSEQ_3:25;
 x = F2 . (y + 1) by A7, A11, A12;
then A14: x in rng F2 by A13, FUNCT_1:def_3;
 rng F2 c= the carrier of G by FINSEQ_1:def_4;
hence  x in the carrier of G by A14; ::_thesis: verum
end;
A15: rng F1 c= the carrier of G by FINSEQ_1:def_4;
 1 <= n + 1 by NAT_1:12;
then  n + 1 in dom F1 by A3, FINSEQ_3:25;
then  F1 . (n + 1) in rng F1 by FUNCT_1:def_3;
then reconsider a = F1 . (n + 1) as Element of G by A15;
A16: F1 = p ^ <*a*> by A3, FINSEQ_3:55;
A17: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_<*(a_")*>_holds_
<*(a_")*>_._k_=_F2_._k
let k be Element of NAT ; ::_thesis: ( k in dom <*(a ")*> implies <*(a ")*> . k = F2 . k )
assume  k in dom <*(a ")*> ; ::_thesis: <*(a ")*> . k = F2 . k
then A18: k in {1} by FINSEQ_1:2, FINSEQ_1:def_8;
 len F2 >= 1 by A3, A4, NAT_1:12;
then A19: len F2 in dom F1 by A4, FINSEQ_3:25;
then  F2 . (((len F1) - (len F1)) + 1) = (F1 /. (len F1)) " by A4, A5;
then  (F1 /. (len F1)) " = F2 . k by A18, TARSKI:def_1;
then A20: F2 . k = a " by A3, A4, A19, PARTFUN1:def_6;
 k = 1 by A18, TARSKI:def_1;
hence  <*(a ")*> . k = F2 . k by A20, FINSEQ_1:def_8; ::_thesis: verum
end;
reconsider q = q as FinSequence of the carrier of G by A10, FINSEQ_1:def_4;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_p_holds_
q_._(((len_p)_-_k)_+_1)_=_(p_/._k)_"
let k be Element of NAT ; ::_thesis: ( k in dom p implies q . (((len p) - k) + 1) = (p /. k) " )
assume A21: k in dom p ; ::_thesis: q . (((len p) - k) + 1) = (p /. k) "
then reconsider i = ((len p) - k) + 1 as Element of NAT by Lm3;
A22: i + 1 = ((len F1) - k) + 1 by A3, A9;
 ( 1 <= i & i <= len p ) by A21, Lm3;
then  i in dom p by FINSEQ_3:25;
then A23: q . i = F2 . (i + 1) by A7, A8;
 k <= len p by A21, FINSEQ_3:25;
then A24: k <= len F1 by A3, A9, NAT_1:12;
 1 <= k by A21, FINSEQ_3:25;
then A25: k in dom F1 by A24, FINSEQ_3:25;
then F1 /. k = F1 . k by PARTFUN1:def_6
.= p . k by A21, FUNCT_1:47
.= p /. k by A21, PARTFUN1:def_6 ;
hence  q . (((len p) - k) + 1) = (p /. k) " by A5, A23, A25, A22; ::_thesis: verum
end;
then A26: Product p = (Product q) " by A2, A9, A6;
A27: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_q_holds_
F2_._((len_<*(a_")*>)_+_k)_=_q_._k
let k be Element of NAT ; ::_thesis: ( k in dom q implies F2 . ((len <*(a ")*>) + k) = q . k )
A28: len <*(a ")*> = 1 by FINSEQ_1:39;
assume  k in dom q ; ::_thesis: F2 . ((len <*(a ")*>) + k) = q . k
hence  F2 . ((len <*(a ")*>) + k) = q . k by A7, A28; ::_thesis: verum
end;
 len F2 = (len <*(a ")*>) + (len q) by A3, A4, A9, A6, FINSEQ_1:39;
then  F2 = <*(a ")*> ^ q by A17, A27, FINSEQ_3:38;
then  Product F2 = (a ") * (Product q) by FINSOP_1:6
.= (a ") * ((Product p) ") by A26
.= ((Product p) * a) " by GROUP_1:17 ;
hence  Product F1 = (Product F2) " by A16, FINSOP_1:4; ::_thesis: verum
end;
A29: S1[ 0 ]
proof
let F1, F2 be FinSequence of the carrier of G; ::_thesis: ( len F1 = 0 & len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " )
assume that
A30: len F1 = 0 and
A31: len F1 = len F2 ; ::_thesis: ( ex k being Element of NAT st
( k in dom F1 & not F2 . (((len F1) - k) + 1) = (F1 /. k) " ) or Product F1 = (Product F2) " )
 F1 = <*> the carrier of G by A30;
then A32: Product F1 = 1_ G by Th8;
 F2 = <*> the carrier of G by A30, A31;
then  Product F2 = 1_ G by Th8;
hence  ( ex k being Element of NAT st
( k in dom F1 & not F2 . (((len F1) - k) + 1) = (F1 /. k) " ) or Product F1 = (Product F2) " ) by A32, GROUP_1:8; ::_thesis: verum
end;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A29, A1);
hence  ( len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " ) ; ::_thesis: verum
end;

theorem :: GROUP_4:15
for G being Group
for F1, F2 being FinSequence of the carrier of G st G is commutative Group holds
for P being Permutation of (dom F1) st F2 = F1 * P holds
Product F1 = Product F2
proof
let G be Group; ::_thesis: for F1, F2 being FinSequence of the carrier of G st G is commutative Group holds
for P being Permutation of (dom F1) st F2 = F1 * P holds
Product F1 = Product F2
let F1, F2 be FinSequence of the carrier of G; ::_thesis: ( G is commutative Group implies for P being Permutation of (dom F1) st F2 = F1 * P holds
Product F1 = Product F2 )
set g = the multF of G;
assume  G is commutative Group ; ::_thesis: for P being Permutation of (dom F1) st F2 = F1 * P holds
Product F1 = Product F2
then  the multF of G is commutative by GROUP_3:2;
hence  for P being Permutation of (dom F1) st F2 = F1 * P holds
Product F1 = Product F2 by FINSOP_1:7; ::_thesis: verum
end;

theorem :: GROUP_4:16
for G being Group
for F1, F2 being FinSequence of the carrier of G st G is commutative Group & F1 is one-to-one & F2 is one-to-one & rng F1 = rng F2 holds
Product F1 = Product F2
proof
let G be Group; ::_thesis: for F1, F2 being FinSequence of the carrier of G st G is commutative Group & F1 is one-to-one & F2 is one-to-one & rng F1 = rng F2 holds
Product F1 = Product F2
let F1, F2 be FinSequence of the carrier of G; ::_thesis: ( G is commutative Group & F1 is one-to-one & F2 is one-to-one & rng F1 = rng F2 implies Product F1 = Product F2 )
set g = the multF of G;
assume  G is commutative Group ; ::_thesis: ( not F1 is one-to-one or not F2 is one-to-one or not rng F1 = rng F2 or Product F1 = Product F2 )
then  the multF of G is commutative by GROUP_3:2;
hence  ( not F1 is one-to-one or not F2 is one-to-one or not rng F1 = rng F2 or Product F1 = Product F2 ) by FINSOP_1:8; ::_thesis: verum
end;

theorem :: GROUP_4:17
for G being Group
for F, F1, F2 being FinSequence of the carrier of G st G is commutative Group & len F = len F1 & len F = len F2 & ( for k being Element of NAT st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ) holds
Product F = (Product F1) * (Product F2)
proof
let G be Group; ::_thesis: for F, F1, F2 being FinSequence of the carrier of G st G is commutative Group & len F = len F1 & len F = len F2 & ( for k being Element of NAT st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ) holds
Product F = (Product F1) * (Product F2)
let F, F1, F2 be FinSequence of the carrier of G; ::_thesis: ( G is commutative Group & len F = len F1 & len F = len F2 & ( for k being Element of NAT st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ) implies Product F = (Product F1) * (Product F2) )
set g = the multF of G;
assume  G is commutative Group ; ::_thesis: ( not len F = len F1 or not len F = len F2 or ex k being Element of NAT st
( k in dom F & not F . k = (F1 /. k) * (F2 /. k) ) or Product F = (Product F1) * (Product F2) )
then A1: the multF of G is commutative by GROUP_3:2;
assume that
A2: len F = len F1 and
A3: len F = len F2 ; ::_thesis: ( ex k being Element of NAT st
( k in dom F & not F . k = (F1 /. k) * (F2 /. k) ) or Product F = (Product F1) * (Product F2) )
assume A4: for k being Element of NAT st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ; ::_thesis: Product F = (Product F1) * (Product F2)
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_F_holds_
F_._k_=_the_multF_of_G_._((F1_._k),(F2_._k))
A5: dom F2 = Seg (len F2) by FINSEQ_1:def_3;
A6: dom F1 = Seg (len F1) by FINSEQ_1:def_3;
let k be Element of NAT ; ::_thesis: ( k in dom F implies F . k = the multF of G . ((F1 . k),(F2 . k)) )
A7: dom F = Seg (len F) by FINSEQ_1:def_3;
assume A8: k in dom F ; ::_thesis: F . k = the multF of G . ((F1 . k),(F2 . k))
hence F . k = (F1 /. k) * (F2 /. k) by A4
.= the multF of G . ((F1 . k),(F2 /. k)) by A2, A8, A7, A6, PARTFUN1:def_6
.= the multF of G . ((F1 . k),(F2 . k)) by A3, A8, A7, A5, PARTFUN1:def_6 ;
::_thesis: verum
end;
hence  Product F = (Product F1) * (Product F2) by A1, A2, A3, FINSOP_1:9; ::_thesis: verum
end;

theorem Th18: :: GROUP_4:18
for G being Group
for H being Subgroup of G
for F being FinSequence of the carrier of G st rng F c= carr H holds
Product F in H
proof
let G be Group; ::_thesis: for H being Subgroup of G
for F being FinSequence of the carrier of G st rng F c= carr H holds
Product F in H
let H be Subgroup of G; ::_thesis: for F being FinSequence of the carrier of G st rng F c= carr H holds
Product F in H
let F be FinSequence of the carrier of G; ::_thesis: ( rng F c= carr H implies Product F in H )
defpred S1[ FinSequence of the carrier of G] means ( rng $1 c= carr H implies Product $1 in H );
A1: now__::_thesis:_for_F_being_FinSequence_of_the_carrier_of_G
for_d_being_Element_of_G_st_S1[F]_holds_
S1[F_^_<*d*>]
let F be FinSequence of the carrier of G; ::_thesis: for d being Element of G st S1[F] holds
S1[F ^ <*d*>]
let d be Element of G; ::_thesis: ( S1[F] implies S1[F ^ <*d*>] )
assume A2: S1[F] ; ::_thesis: S1[F ^ <*d*>]
thus  S1[F ^ <*d*>] ::_thesis: verum
proof
A3: ( rng F c= rng (F ^ <*d*>) & Product (F ^ <*d*>) = (Product F) * d ) by FINSEQ_1:29, FINSOP_1:4;
A4: ( rng <*d*> = {d} & d in {d} ) by FINSEQ_1:39, TARSKI:def_1;
assume A5: rng (F ^ <*d*>) c= carr H ; ::_thesis: Product (F ^ <*d*>) in H
 rng <*d*> c= rng (F ^ <*d*>) by FINSEQ_1:30;
then  rng <*d*> c= carr H by A5, XBOOLE_1:1;
then  d in H by A4, STRUCT_0:def_5;
hence  Product (F ^ <*d*>) in H by A2, A5, A3, GROUP_2:50, XBOOLE_1:1; ::_thesis: verum
end;
end;
A6: S1[ <*> the carrier of G]
proof
assume  rng (<*> the carrier of G) c= carr H ; ::_thesis: Product (<*> the carrier of G) in H
 1_ G in H by GROUP_2:46;
hence  Product (<*> the carrier of G) in H by Th8; ::_thesis: verum
end;
 for F being FinSequence of the carrier of G holds S1[F] from FINSEQ_2:sch_2(A6, A1);
hence  ( rng F c= carr H implies Product F in H ) ; ::_thesis: verum
end;

definition
let G be Group;
let I be FinSequence of INT ;
let F be FinSequence of the carrier of G;
funcF |^ I ->  FinSequence of the carrier of G means :Def3: :: GROUP_4:def 3
( len it = len F & ( for k being Element of NAT st k in dom F holds
it . k = (F /. k) |^ (@ (I /. k)) ) );
existence
 ex b1 being FinSequence of the carrier of G st
( len b1 = len F & ( for k being Element of NAT st k in dom F holds
b1 . k = (F /. k) |^ (@ (I /. k)) ) )
proof
deffunc H1( Nat) ->  Element of the carrier of G = (F /. $1) |^ (@ (I /. $1));
consider p being FinSequence such that
A1: len p = len F and
A2: for k being Nat st k in dom p holds
p . k = H1(k) from FINSEQ_1:sch_2();
A3: dom p = dom F by A1, FINSEQ_3:29;
 rng p c= the carrier of G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in the carrier of G )
assume  x in rng p ; ::_thesis: x in the carrier of G
then consider y being set  such that
A4: y in dom p and
A5: p . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A4;
 x = (F /. y) |^ (@ (I /. y)) by A2, A4, A5;
hence  x in the carrier of G ; ::_thesis: verum
end;
then reconsider p = p as FinSequence of the carrier of G by FINSEQ_1:def_4;
take  p ; ::_thesis: ( len p = len F & ( for k being Element of NAT st k in dom F holds
p . k = (F /. k) |^ (@ (I /. k)) ) )
thus  ( len p = len F & ( for k being Element of NAT st k in dom F holds
p . k = (F /. k) |^ (@ (I /. k)) ) ) by A1, A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of the carrier of G st len b1 = len F & ( for k being Element of NAT st k in dom F holds
b1 . k = (F /. k) |^ (@ (I /. k)) ) & len b2 = len F & ( for k being Element of NAT st k in dom F holds
b2 . k = (F /. k) |^ (@ (I /. k)) ) holds
b1 = b2
proof
let F1, F2 be FinSequence of the carrier of G; ::_thesis: ( len F1 = len F & ( for k being Element of NAT st k in dom F holds
F1 . k = (F /. k) |^ (@ (I /. k)) ) & len F2 = len F & ( for k being Element of NAT st k in dom F holds
F2 . k = (F /. k) |^ (@ (I /. k)) ) implies F1 = F2 )
assume that
A6: len F1 = len F and
A7: for k being Element of NAT st k in dom F holds
F1 . k = (F /. k) |^ (@ (I /. k)) ; ::_thesis: ( not len F2 = len F or ex k being Element of NAT st
( k in dom F & not F2 . k = (F /. k) |^ (@ (I /. k)) ) or F1 = F2 )
assume that
A8: len F2 = len F and
A9: for k being Element of NAT st k in dom F holds
F2 . k = (F /. k) |^ (@ (I /. k)) ; ::_thesis: F1 = F2
A10: dom F1 = Seg (len F) by A6, FINSEQ_1:def_3;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_F1_holds_
F1_._k_=_F2_._k
let k be Nat; ::_thesis: ( k in dom F1 implies F1 . k = F2 . k )
assume  k in dom F1 ; ::_thesis: F1 . k = F2 . k
then A11: k in dom F by A10, FINSEQ_1:def_3;
hence F1 . k = (F /. k) |^ (@ (I /. k)) by A7
.= F2 . k by A9, A11 ;
::_thesis: verum
end;
hence  F1 = F2 by A6, A8, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines |^ GROUP_4:def_3_:_
 for G being Group
for I being FinSequence of INT
for F, b4 being FinSequence of the carrier of G holds
( b4 = F |^ I iff ( len b4 = len F & ( for k being Element of NAT st k in dom F holds
b4 . k = (F /. k) |^ (@ (I /. k)) ) ) );

theorem Th19: :: GROUP_4:19
for G being Group
for F1, F2 being FinSequence of the carrier of G
for I1, I2 being FinSequence of INT st len F1 = len I1 & len F2 = len I2 holds
(F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2)
proof
let G be Group; ::_thesis: for F1, F2 being FinSequence of the carrier of G
for I1, I2 being FinSequence of INT st len F1 = len I1 & len F2 = len I2 holds
(F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2)
let F1, F2 be FinSequence of the carrier of G; ::_thesis: for I1, I2 being FinSequence of INT st len F1 = len I1 & len F2 = len I2 holds
(F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2)
let I1, I2 be FinSequence of INT ; ::_thesis: ( len F1 = len I1 & len F2 = len I2 implies (F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2) )
assume that
A1: len F1 = len I1 and
A2: len F2 = len I2 ; ::_thesis: (F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2)
set r = F2 |^ I2;
set q = F1 |^ I1;
len (F1 ^ F2) = (len F1) + (len F2) by FINSEQ_1:22
.= len (I1 ^ I2) by A1, A2, FINSEQ_1:22 ;
then A3: dom (F1 ^ F2) = dom (I1 ^ I2) by FINSEQ_3:29;
A4: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(F1_^_F2)_holds_
((F1_|^_I1)_^_(F2_|^_I2))_._k_=_((F1_^_F2)_/._k)_|^_(@_((I1_^_I2)_/._k))
let k be Element of NAT ; ::_thesis: ( k in dom (F1 ^ F2) implies ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k)) )
assume A5: k in dom (F1 ^ F2) ; ::_thesis: ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k))
now__::_thesis:_((F1_|^_I1)_^_(F2_|^_I2))_._k_=_((F1_^_F2)_/._k)_|^_(@_((I1_^_I2)_/._k))
percases ( k in dom F1 or ex n being Nat st
( n in dom F2 & k = (len F1) + n ) ) by A5, FINSEQ_1:25;
supposeA6: k in dom F1 ; ::_thesis: ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k))
 len (F1 |^ I1) = len F1 by Def3;
then  k in dom (F1 |^ I1) by A6, FINSEQ_3:29;
then A7: ((F1 |^ I1) ^ (F2 |^ I2)) . k = (F1 |^ I1) . k by FINSEQ_1:def_7
.= (F1 /. k) |^ (@ (I1 /. k)) by A6, Def3 ;
A8: (I1 ^ I2) . k = (I1 ^ I2) /. k by A3, A5, PARTFUN1:def_6;
A9: F1 /. k = F1 . k by A6, PARTFUN1:def_6
.= (F1 ^ F2) . k by A6, FINSEQ_1:def_7
.= (F1 ^ F2) /. k by A5, PARTFUN1:def_6 ;
A10: k in dom I1 by A1, A6, FINSEQ_3:29;
then  I1 /. k = I1 . k by PARTFUN1:def_6;
hence  ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k)) by A10, A8, A7, A9, FINSEQ_1:def_7; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom F2 & k = (len F1) + n ) ; ::_thesis: ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k))
then consider n being Element of NAT  such that
A11: n in dom F2 and
A12: k = (len F1) + n ;
A13: ( (F1 ^ F2) . k = F2 . n & F2 . n = F2 /. n ) by A11, A12, FINSEQ_1:def_7, PARTFUN1:def_6;
A14: len (F1 |^ I1) = len F1 by Def3;
 len (F2 |^ I2) = len F2 by Def3;
then  n in dom (F2 |^ I2) by A11, FINSEQ_3:29;
then A15: ((F1 |^ I1) ^ (F2 |^ I2)) . k = (F2 |^ I2) . n by A12, A14, FINSEQ_1:def_7;
A16: ( (F1 ^ F2) . k = (F1 ^ F2) /. k & (I1 ^ I2) /. k = (I1 ^ I2) . k ) by A3, A5, PARTFUN1:def_6;
A17: n in dom I2 by A2, A11, FINSEQ_3:29;
then A18: I2 /. n = I2 . n by PARTFUN1:def_6;
 (I1 ^ I2) . k = I2 . n by A1, A12, A17, FINSEQ_1:def_7;
hence  ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k)) by A11, A15, A13, A16, A18, Def3; ::_thesis: verum
end;
end;
end;
hence  ((F1 |^ I1) ^ (F2 |^ I2)) . k = ((F1 ^ F2) /. k) |^ (@ ((I1 ^ I2) /. k)) ; ::_thesis: verum
end;
len ((F1 |^ I1) ^ (F2 |^ I2)) = (len (F1 |^ I1)) + (len (F2 |^ I2)) by FINSEQ_1:22
.= (len F1) + (len (F2 |^ I2)) by Def3
.= (len F1) + (len F2) by Def3
.= len (F1 ^ F2) by FINSEQ_1:22 ;
hence  (F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2) by A4, Def3; ::_thesis: verum
end;

theorem Th20: :: GROUP_4:20
for G being Group
for H being Subgroup of G
for F being FinSequence of the carrier of G
for I being FinSequence of INT st rng F c= carr H holds
Product (F |^ I) in H
proof
let G be Group; ::_thesis: for H being Subgroup of G
for F being FinSequence of the carrier of G
for I being FinSequence of INT st rng F c= carr H holds
Product (F |^ I) in H
let H be Subgroup of G; ::_thesis: for F being FinSequence of the carrier of G
for I being FinSequence of INT st rng F c= carr H holds
Product (F |^ I) in H
let F be FinSequence of the carrier of G; ::_thesis: for I being FinSequence of INT st rng F c= carr H holds
Product (F |^ I) in H
let I be FinSequence of INT ; ::_thesis: ( rng F c= carr H implies Product (F |^ I) in H )
assume A1: rng F c= carr H ; ::_thesis: Product (F |^ I) in H
 rng (F |^ I) c= carr H
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (F |^ I) or x in carr H )
assume  x in rng (F |^ I) ; ::_thesis: x in carr H
then consider y being set  such that
A2: y in dom (F |^ I) and
A3: x = (F |^ I) . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A2;
 len (F |^ I) = len F by Def3;
then A4: y in dom F by A2, FINSEQ_3:29;
then  ( F . y in rng F & F . y = F /. y ) by FUNCT_1:def_3, PARTFUN1:def_6;
then A5: F /. y in H by A1, STRUCT_0:def_5;
 x = (F /. y) |^ (@ (I /. y)) by A3, A4, Def3;
then  x in H by A5, Th4;
hence  x in carr H by STRUCT_0:def_5; ::_thesis: verum
end;
hence  Product (F |^ I) in H by Th18; ::_thesis: verum
end;

theorem Th21: :: GROUP_4:21
for G being Group holds (<*> the carrier of G) |^ (<*> INT) = {}
proof
let G be Group; ::_thesis: (<*> the carrier of G) |^ (<*> INT) = {}
 len (<*> the carrier of G) = 0 ;
then  len ((<*> the carrier of G) |^ (<*> INT)) = 0 by Def3;
hence  (<*> the carrier of G) |^ (<*> INT) = {} ; ::_thesis: verum
end;

theorem Th22: :: GROUP_4:22
for i being Integer
for G being Group
for a being Element of G holds <*a*> |^ <*(@ i)*> = <*(a |^ i)*>
proof
let i be Integer; ::_thesis: for G being Group
for a being Element of G holds <*a*> |^ <*(@ i)*> = <*(a |^ i)*>
let G be Group; ::_thesis: for a being Element of G holds <*a*> |^ <*(@ i)*> = <*(a |^ i)*>
let a be Element of G; ::_thesis: <*a*> |^ <*(@ i)*> = <*(a |^ i)*>
A1: len <*a*> = 1 by FINSEQ_1:39;
A2: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_<*a*>_holds_
<*(a_|^_i)*>_._k_=_(<*a*>_/._k)_|^_(@_(<*(@_i)*>_/._k))
let k be Element of NAT ; ::_thesis: ( k in dom <*a*> implies <*(a |^ i)*> . k = (<*a*> /. k) |^ (@ (<*(@ i)*> /. k)) )
A3: @ i = <*(@ i)*> /. 1 by FINSEQ_4:16;
A4: dom <*a*> = Seg (len <*a*>) by FINSEQ_1:def_3;
assume  k in dom <*a*> ; ::_thesis: <*(a |^ i)*> . k = (<*a*> /. k) |^ (@ (<*(@ i)*> /. k))
then A5: k = 1 by A1, A4, FINSEQ_1:2, TARSKI:def_1;
hence <*(a |^ i)*> . k = a |^ i by FINSEQ_1:40
.= (<*a*> /. k) |^ (@ (<*(@ i)*> /. k)) by A3, A5, FINSEQ_4:16 ;
::_thesis: verum
end;
 len <*(a |^ i)*> = 1 by FINSEQ_1:39;
hence  <*a*> |^ <*(@ i)*> = <*(a |^ i)*> by A1, A2, Def3; ::_thesis: verum
end;

theorem Th23: :: GROUP_4:23
for i, j being Integer
for G being Group
for a, b being Element of G holds <*a,b*> |^ <*(@ i),(@ j)*> = <*(a |^ i),(b |^ j)*>
proof
let i, j be Integer; ::_thesis: for G being Group
for a, b being Element of G holds <*a,b*> |^ <*(@ i),(@ j)*> = <*(a |^ i),(b |^ j)*>
let G be Group; ::_thesis: for a, b being Element of G holds <*a,b*> |^ <*(@ i),(@ j)*> = <*(a |^ i),(b |^ j)*>
let a, b be Element of G; ::_thesis: <*a,b*> |^ <*(@ i),(@ j)*> = <*(a |^ i),(b |^ j)*>
A1: ( len <*(@ i)*> = 1 & len <*(@ j)*> = 1 ) by FINSEQ_1:39;
A2: ( <*a,b*> = <*a*> ^ <*b*> & <*(@ i),(@ j)*> = <*(@ i)*> ^ <*(@ j)*> ) by FINSEQ_1:def_9;
 ( len <*a*> = 1 & len <*b*> = 1 ) by FINSEQ_1:39;
hence <*a,b*> |^ <*(@ i),(@ j)*> = (<*a*> |^ <*(@ i)*>) ^ (<*b*> |^ <*(@ j)*>) by A1, A2, Th19
.= <*(a |^ i)*> ^ (<*b*> |^ <*(@ j)*>) by Th22
.= <*(a |^ i)*> ^ <*(b |^ j)*> by Th22
.= <*(a |^ i),(b |^ j)*> by FINSEQ_1:def_9 ;
::_thesis: verum
end;

theorem :: GROUP_4:24
for i1, i2, i3 being Integer
for G being Group
for a, b, c being Element of G holds <*a,b,c*> |^ <*(@ i1),(@ i2),(@ i3)*> = <*(a |^ i1),(b |^ i2),(c |^ i3)*>
proof
let i1, i2, i3 be Integer; ::_thesis: for G being Group
for a, b, c being Element of G holds <*a,b,c*> |^ <*(@ i1),(@ i2),(@ i3)*> = <*(a |^ i1),(b |^ i2),(c |^ i3)*>
let G be Group; ::_thesis: for a, b, c being Element of G holds <*a,b,c*> |^ <*(@ i1),(@ i2),(@ i3)*> = <*(a |^ i1),(b |^ i2),(c |^ i3)*>
let a, b, c be Element of G; ::_thesis: <*a,b,c*> |^ <*(@ i1),(@ i2),(@ i3)*> = <*(a |^ i1),(b |^ i2),(c |^ i3)*>
A1: ( len <*(@ i1)*> = 1 & len <*(@ i2),(@ i3)*> = 2 ) by FINSEQ_1:39, FINSEQ_1:44;
A2: ( <*a,b,c*> = <*a*> ^ <*b,c*> & <*(@ i1),(@ i2),(@ i3)*> = <*(@ i1)*> ^ <*(@ i2),(@ i3)*> ) by FINSEQ_1:43;
 ( len <*a*> = 1 & len <*b,c*> = 2 ) by FINSEQ_1:39, FINSEQ_1:44;
hence <*a,b,c*> |^ <*(@ i1),(@ i2),(@ i3)*> = (<*a*> |^ <*(@ i1)*>) ^ (<*b,c*> |^ <*(@ i2),(@ i3)*>) by A1, A2, Th19
.= <*(a |^ i1)*> ^ (<*b,c*> |^ <*(@ i2),(@ i3)*>) by Th22
.= <*(a |^ i1)*> ^ <*(b |^ i2),(c |^ i3)*> by Th23
.= <*(a |^ i1),(b |^ i2),(c |^ i3)*> by FINSEQ_1:43 ;
::_thesis: verum
end;

theorem :: GROUP_4:25
for G being Group
for F being FinSequence of the carrier of G holds F |^ ((len F) |-> (@ 1)) = F
proof
let G be Group; ::_thesis: for F being FinSequence of the carrier of G holds F |^ ((len F) |-> (@ 1)) = F
let F be FinSequence of the carrier of G; ::_thesis: F |^ ((len F) |-> (@ 1)) = F
defpred S1[ FinSequence of the carrier of G] means $1 |^ ((len $1) |-> (@ 1)) = $1;
A1: for F being FinSequence of the carrier of G
for a being Element of G st S1[F] holds
S1[F ^ <*a*>]
proof
let F be FinSequence of the carrier of G; ::_thesis: for a being Element of G st S1[F] holds
S1[F ^ <*a*>]
let a be Element of G; ::_thesis: ( S1[F] implies S1[F ^ <*a*>] )
set A = F ^ <*a*>;
assume A2: S1[F] ; ::_thesis: S1[F ^ <*a*>]
A3: len <*a*> = 1 by FINSEQ_1:40;
A4: ( len <*(@ 1)*> = 1 & len ((len F) |-> (@ 1)) = len F ) by CARD_1:def_7;
 len (F ^ <*a*>) = (len F) + (len <*a*>) by FINSEQ_1:22;
hence (F ^ <*a*>) |^ ((len (F ^ <*a*>)) |-> (@ 1)) = (F ^ <*a*>) |^ (((len F) |-> (@ 1)) ^ <*(@ 1)*>) by A3, FINSEQ_2:60
.= (F |^ ((len F) |-> (@ 1))) ^ (<*a*> |^ <*(@ 1)*>) by A3, A4, Th19
.= F ^ <*(a |^ 1)*> by A2, Th22
.= F ^ <*a*> by GROUP_1:26 ;
::_thesis: verum
end;
A5: S1[ <*> the carrier of G]
proof
set A = <*> the carrier of G;
thus (<*> the carrier of G) |^ ((len (<*> the carrier of G)) |-> (@ 1)) = (<*> the carrier of G) |^ (0 |-> (@ 1))
.= (<*> the carrier of G) |^ (<*> INT)
.= <*> the carrier of G by Th21 ; ::_thesis: verum
end;
 for F being FinSequence of the carrier of G holds S1[F] from FINSEQ_2:sch_2(A5, A1);
hence  F |^ ((len F) |-> (@ 1)) = F ; ::_thesis: verum
end;

theorem :: GROUP_4:26
for G being Group
for F being FinSequence of the carrier of G holds F |^ ((len F) |-> (@ 0)) = (len F) |-> (1_ G)
proof
let G be Group; ::_thesis: for F being FinSequence of the carrier of G holds F |^ ((len F) |-> (@ 0)) = (len F) |-> (1_ G)
let F be FinSequence of the carrier of G; ::_thesis: F |^ ((len F) |-> (@ 0)) = (len F) |-> (1_ G)
defpred S1[ FinSequence of the carrier of G] means $1 |^ ((len $1) |-> (@ 0)) = (len $1) |-> (1_ G);
A1: for F being FinSequence of the carrier of G
for a being Element of G st S1[F] holds
S1[F ^ <*a*>]
proof
let F be FinSequence of the carrier of G; ::_thesis: for a being Element of G st S1[F] holds
S1[F ^ <*a*>]
let a be Element of G; ::_thesis: ( S1[F] implies S1[F ^ <*a*>] )
set A = F ^ <*a*>;
assume A2: S1[F] ; ::_thesis: S1[F ^ <*a*>]
A3: len <*a*> = 1 by FINSEQ_1:40;
A4: ( len <*(@ 0)*> = 1 & len ((len F) |-> (@ 0)) = len F ) by CARD_1:def_7;
A5: len (F ^ <*a*>) = (len F) + (len <*a*>) by FINSEQ_1:22;
hence (F ^ <*a*>) |^ ((len (F ^ <*a*>)) |-> (@ 0)) = (F ^ <*a*>) |^ (((len F) |-> (@ 0)) ^ <*(@ 0)*>) by A3, FINSEQ_2:60
.= (F |^ ((len F) |-> (@ 0))) ^ (<*a*> |^ <*(@ 0)*>) by A3, A4, Th19
.= ((len F) |-> (1_ G)) ^ <*(a |^ 0)*> by A2, Th22
.= ((len F) |-> (1_ G)) ^ <*(1_ G)*> by GROUP_1:25
.= (len (F ^ <*a*>)) |-> (1_ G) by A5, A3, FINSEQ_2:60 ;
::_thesis: verum
end;
A6: S1[ <*> the carrier of G]
proof
set A = <*> the carrier of G;
thus (<*> the carrier of G) |^ ((len (<*> the carrier of G)) |-> (@ 0)) = (<*> the carrier of G) |^ (0 |-> (@ 0))
.= (<*> the carrier of G) |^ (<*> INT)
.= {} by Th21
.= (len (<*> the carrier of G)) |-> (1_ G) ; ::_thesis: verum
end;
 for F being FinSequence of the carrier of G holds S1[F] from FINSEQ_2:sch_2(A6, A1);
hence  F |^ ((len F) |-> (@ 0)) = (len F) |-> (1_ G) ; ::_thesis: verum
end;

theorem :: GROUP_4:27
for n being Element of NAT
for G being Group
for I being FinSequence of INT st len I = n holds
(n |-> (1_ G)) |^ I = n |-> (1_ G)
proof
let n be Element of NAT ; ::_thesis: for G being Group
for I being FinSequence of INT st len I = n holds
(n |-> (1_ G)) |^ I = n |-> (1_ G)
let G be Group; ::_thesis: for I being FinSequence of INT st len I = n holds
(n |-> (1_ G)) |^ I = n |-> (1_ G)
let I be FinSequence of INT ; ::_thesis: ( len I = n implies (n |-> (1_ G)) |^ I = n |-> (1_ G) )
defpred S1[ Element of NAT ] means  for I being FinSequence of INT st len I = $1 holds
($1 |-> (1_ G)) |^ I = $1 |-> (1_ G);
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
let I be FinSequence of INT ; ::_thesis: ( len I = k + 1 implies ((k + 1) |-> (1_ G)) |^ I = (k + 1) |-> (1_ G) )
reconsider J = I | (Seg k) as FinSequence of INT by FINSEQ_1:18;
assume A3: len I = k + 1 ; ::_thesis: ((k + 1) |-> (1_ G)) |^ I = (k + 1) |-> (1_ G)
then A4: len J = k by FINSEQ_3:53;
then A5: (k |-> (1_ G)) |^ J = k |-> (1_ G) by A2;
A6: rng I c= INT by FINSEQ_1:def_4;
 1 <= k + 1 by NAT_1:12;
then  k + 1 in dom I by A3, FINSEQ_3:25;
then  I . (k + 1) in rng I by FUNCT_1:def_3;
then reconsider i = I . (k + 1) as Integer by A6;
A7: ( len <*(1_ G)*> = 1 & len <*(@ i)*> = 1 ) by FINSEQ_1:40;
A8: ( (k + 1) |-> (1_ G) = (k |-> (1_ G)) ^ <*(1_ G)*> & len (k |-> (1_ G)) = k ) by CARD_1:def_7, FINSEQ_2:60;
 I = J ^ <*(@ i)*> by A3, FINSEQ_3:55;
then ((k + 1) |-> (1_ G)) |^ I = ((k |-> (1_ G)) |^ J) ^ (<*(1_ G)*> |^ <*(@ i)*>) by A4, A8, A7, Th19
.= (k |-> (1_ G)) ^ <*((1_ G) |^ i)*> by A5, Th22
.= (k |-> (1_ G)) ^ <*(1_ G)*> by GROUP_1:31 ;
hence  ((k + 1) |-> (1_ G)) |^ I = (k + 1) |-> (1_ G) by FINSEQ_2:60; ::_thesis: verum
end;
A9: S1[ 0 ]
proof
let I be FinSequence of INT ; ::_thesis: ( len I = 0 implies (0 |-> (1_ G)) |^ I = 0 |-> (1_ G) )
assume  len I = 0 ; ::_thesis: (0 |-> (1_ G)) |^ I = 0 |-> (1_ G)
then A10: I = <*> INT ;
 {} = <*> the carrier of G ;
hence  (0 |-> (1_ G)) |^ I = 0 |-> (1_ G) by A10, Th21; ::_thesis: verum
end;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A9, A1);
hence  ( len I = n implies (n |-> (1_ G)) |^ I = n |-> (1_ G) ) ; ::_thesis: verum
end;

definition
let G be Group;
let A be Subset of G;
func gr A ->  strict Subgroup of G means :Def4: :: GROUP_4:def 4
( A c= the carrier of it & ( for H being strict Subgroup of G st A c= the carrier of H holds
it is Subgroup of H ) );
existence
 ex b1 being strict Subgroup of G st
( A c= the carrier of b1 & ( for H being strict Subgroup of G st A c= the carrier of H holds
b1 is Subgroup of H ) )
proof
defpred S1[ set ] means  ex H being Subgroup of G st
( $1 = carr H & A c= $1 );
consider X being set  such that
A1: for Y being set holds
( Y in X iff ( Y in bool the carrier of G & S1[Y] ) ) from XBOOLE_0:sch_1();
set M = meet X;
A2: carr ((Omega). G) = the carrier of ((Omega). G) ;
then A3: X <> {} by A1;
A4: the carrier of G in X by A1, A2;
A5: meet X c= the carrier of G
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in meet X or y in the carrier of G )
consider x being set  such that
A6: x in X by A4;
consider H being Subgroup of G such that
A7: x = carr H and
 A c= x by A1, A6;
assume  y in meet X ; ::_thesis: y in the carrier of G
then  y in carr H by A6, A7, SETFAM_1:def_1;
hence  y in the carrier of G ; ::_thesis: verum
end;
now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
1__G_in_Y
let Y be set ; ::_thesis: ( Y in X implies 1_ G in Y )
assume  Y in X ; ::_thesis: 1_ G in Y
then consider H being Subgroup of G such that
A8: Y = carr H and
 A c= Y by A1;
 1_ G in H by GROUP_2:46;
hence  1_ G in Y by A8, STRUCT_0:def_5; ::_thesis: verum
end;
then A9: meet X <> {} by A3, SETFAM_1:def_1;
reconsider M = meet X as Subset of G by A5;
A10: now__::_thesis:_for_a,_b_being_Element_of_G_st_a_in_M_&_b_in_M_holds_
a_*_b_in_M
let a, b be Element of G; ::_thesis: ( a in M & b in M implies a * b in M )
assume A11: ( a in M & b in M ) ; ::_thesis: a * b in M
now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
a_*_b_in_Y
let Y be set ; ::_thesis: ( Y in X implies a * b in Y )
assume A12: Y in X ; ::_thesis: a * b in Y
then consider H being Subgroup of G such that
A13: Y = carr H and
 A c= Y by A1;
 ( a in carr H & b in carr H ) by A11, A12, A13, SETFAM_1:def_1;
hence  a * b in Y by A13, GROUP_2:74; ::_thesis: verum
end;
hence  a * b in M by A3, SETFAM_1:def_1; ::_thesis: verum
end;
now__::_thesis:_for_a_being_Element_of_G_st_a_in_M_holds_
a_"_in_M
let a be Element of G; ::_thesis: ( a in M implies a " in M )
assume A14: a in M ; ::_thesis: a " in M
now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
a_"_in_Y
let Y be set ; ::_thesis: ( Y in X implies a " in Y )
assume A15: Y in X ; ::_thesis: a " in Y
then consider H being Subgroup of G such that
A16: Y = carr H and
 A c= Y by A1;
 a in carr H by A14, A15, A16, SETFAM_1:def_1;
hence  a " in Y by A16, GROUP_2:75; ::_thesis: verum
end;
hence  a " in M by A3, SETFAM_1:def_1; ::_thesis: verum
end;
then consider H being strict Subgroup of G such that
A17: the carrier of H = M by A9, A10, GROUP_2:52;
take  H ; ::_thesis: ( A c= the carrier of H & ( for H being strict Subgroup of G st A c= the carrier of H holds
H is Subgroup of H ) )
now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
A_c=_Y
let Y be set ; ::_thesis: ( Y in X implies A c= Y )
assume  Y in X ; ::_thesis: A c= Y
then  ex H being Subgroup of G st
( Y = carr H & A c= Y ) by A1;
hence  A c= Y ; ::_thesis: verum
end;
hence  A c= the carrier of H by A3, A17, SETFAM_1:5; ::_thesis: for H being strict Subgroup of G st A c= the carrier of H holds
H is Subgroup of H
let H1 be strict Subgroup of G; ::_thesis: ( A c= the carrier of H1 implies H is Subgroup of H1 )
A18: the carrier of H1 = carr H1 ;
assume  A c= the carrier of H1 ; ::_thesis: H is Subgroup of H1
then  the carrier of H1 in X by A1, A18;
hence  H is Subgroup of H1 by A17, GROUP_2:57, SETFAM_1:3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Subgroup of G st A c= the carrier of b1 & ( for H being strict Subgroup of G st A c= the carrier of H holds
b1 is Subgroup of H ) & A c= the carrier of b2 & ( for H being strict Subgroup of G st A c= the carrier of H holds
b2 is Subgroup of H ) holds
b1 = b2
proof
let H1, H2 be strict Subgroup of G; ::_thesis: ( A c= the carrier of H1 & ( for H being strict Subgroup of G st A c= the carrier of H holds
H1 is Subgroup of H ) & A c= the carrier of H2 & ( for H being strict Subgroup of G st A c= the carrier of H holds
H2 is Subgroup of H ) implies H1 = H2 )
assume  ( A c= the carrier of H1 & ( for H being strict Subgroup of G st A c= the carrier of H holds
H1 is Subgroup of H ) & A c= the carrier of H2 & ( for H being strict Subgroup of G st A c= the carrier of H holds
H2 is Subgroup of H ) ) ; ::_thesis: H1 = H2
then  ( H1 is Subgroup of H2 & H2 is Subgroup of H1 ) ;
hence  H1 = H2 by GROUP_2:55; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines gr GROUP_4:def_4_:_
 for G being Group
for A being Subset of G
for b3 being strict Subgroup of G holds
( b3 = gr A iff ( A c= the carrier of b3 & ( for H being strict Subgroup of G st A c= the carrier of H holds
b3 is Subgroup of H ) ) );

theorem Th28: :: GROUP_4:28
for G being Group
for a being Element of G
for A being Subset of G holds
( a in gr A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) )
proof
let G be Group; ::_thesis: for a being Element of G
for A being Subset of G holds
( a in gr A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) )
let a be Element of G; ::_thesis: for A being Subset of G holds
( a in gr A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) )
let A be Subset of G; ::_thesis: ( a in gr A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) )
thus  ( a in gr A implies ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) ) ::_thesis: ( ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) implies a in gr A )
proof
defpred S1[ set ] means  ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( $1 = Product (F |^ I) & len F = len I & rng F c= A );
assume A1: a in gr A ; ::_thesis: ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a )
reconsider B =  {  b where b is Element of G : S1[b]  }  as Subset of G from DOMAIN_1:sch_7();
A2: now__::_thesis:_for_c,_d_being_Element_of_G_st_c_in_B_&_d_in_B_holds_
c_*_d_in_B
let c, d be Element of G; ::_thesis: ( c in B & d in B implies c * d in B )
assume that
A3: c in B and
A4: d in B ; ::_thesis: c * d in B
 ex d1 being Element of G st
( c = d1 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( d1 = Product (F |^ I) & len F = len I & rng F c= A ) ) by A3;
then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT  such that
A5: c = Product (F1 |^ I1) and
A6: len F1 = len I1 and
A7: rng F1 c= A ;
 ex d2 being Element of G st
( d = d2 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( d2 = Product (F |^ I) & len F = len I & rng F c= A ) ) by A4;
then consider F2 being FinSequence of the carrier of G, I2 being FinSequence of INT  such that
A8: d = Product (F2 |^ I2) and
A9: len F2 = len I2 and
A10: rng F2 c= A ;
A11: len (F1 ^ F2) = (len I1) + (len I2) by A6, A9, FINSEQ_1:22
.= len (I1 ^ I2) by FINSEQ_1:22 ;
 rng (F1 ^ F2) = (rng F1) \/ (rng F2) by FINSEQ_1:31;
then A12: rng (F1 ^ F2) c= A by A7, A10, XBOOLE_1:8;
c * d = Product ((F1 |^ I1) ^ (F2 |^ I2)) by A5, A8, FINSOP_1:5
.= Product ((F1 ^ F2) |^ (I1 ^ I2)) by A6, A9, Th19 ;
hence  c * d in B by A12, A11; ::_thesis: verum
end;
A13: now__::_thesis:_for_c_being_Element_of_G_st_c_in_B_holds_
c_"_in_B
let c be Element of G; ::_thesis: ( c in B implies c " in B )
assume  c in B ; ::_thesis: c " in B
then  ex d1 being Element of G st
( c = d1 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( d1 = Product (F |^ I) & len F = len I & rng F c= A ) ) ;
then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT  such that
A14: c = Product (F1 |^ I1) and
A15: len F1 = len I1 and
A16: rng F1 c= A ;
deffunc H1( Nat) ->  set = F1 . (((len F1) - $1) + 1);
consider F2 being FinSequence such that
A17: len F2 = len F1 and
A18: for k being Nat st k in dom F2 holds
F2 . k = H1(k) from FINSEQ_1:sch_2();
A19: Seg (len I1) = dom I1 by FINSEQ_1:def_3;
A20: rng F2 c= rng F1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F2 or x in rng F1 )
assume  x in rng F2 ; ::_thesis: x in rng F1
then consider y being set  such that
A21: y in dom F2 and
A22: F2 . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A21;
reconsider n = ((len F1) - y) + 1 as Element of NAT by A17, A21, Lm3;
 ( 1 <= n & n <= len F1 ) by A17, A21, Lm3;
then A23: n in dom F1 by FINSEQ_3:25;
 x = F1 . (((len F1) - y) + 1) by A18, A21, A22;
hence  x in rng F1 by A23, FUNCT_1:def_3; ::_thesis: verum
end;
then A24: rng F2 c= A by A16, XBOOLE_1:1;
defpred S2[ Nat, set ] means  ex i being Integer st
( i = I1 . (((len I1) - $1) + 1) & $2 = - i );
A25: for k being Nat st k in Seg (len I1) holds
ex x being set st S2[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len I1) implies ex x being set st S2[k,x] )
assume  k in Seg (len I1) ; ::_thesis: ex x being set st S2[k,x]
then A26: k in dom I1 by FINSEQ_1:def_3;
then reconsider n = ((len I1) - k) + 1 as Element of NAT by Lm3;
 ( 1 <= n & n <= len I1 ) by A26, Lm3;
then  n in dom I1 by FINSEQ_3:25;
then A27: I1 . n in rng I1 by FUNCT_1:def_3;
 rng I1 c= INT by FINSEQ_1:def_4;
then reconsider i = I1 . n as Element of INT by A27;
reconsider i = i as Integer ;
reconsider x = - i as set ;
take  x ; ::_thesis: S2[k,x]
take  i ; ::_thesis: ( i = I1 . (((len I1) - k) + 1) & x = - i )
thus  ( i = I1 . (((len I1) - k) + 1) & x = - i ) ; ::_thesis: verum
end;
consider I2 being FinSequence such that
A28: dom I2 = Seg (len I1) and
A29: for k being Nat st k in Seg (len I1) holds
S2[k,I2 . k] from FINSEQ_1:sch_1(A25);
A30: len F2 = len I2 by A15, A17, A28, FINSEQ_1:def_3;
A31: rng I2 c= INT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng I2 or x in INT )
assume  x in rng I2 ; ::_thesis: x in INT
then consider y being set  such that
A32: y in dom I2 and
A33: x = I2 . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A32;
 ex i being Integer st
( i = I1 . (((len I1) - y) + 1) & x = - i ) by A28, A29, A32, A33;
hence  x in INT by INT_1:def_2; ::_thesis: verum
end;
 rng F1 c= the carrier of G by FINSEQ_1:def_4;
then A34: rng F2 c= the carrier of G by A20, XBOOLE_1:1;
set p = F1 |^ I1;
A35: Seg (len F1) = dom F1 by FINSEQ_1:def_3;
A36: len (F1 |^ I1) = len F1 by Def3;
A37: dom F2 = dom I2 by A15, A17, A28, FINSEQ_1:def_3;
reconsider I2 = I2 as FinSequence of INT by A31, FINSEQ_1:def_4;
reconsider F2 = F2 as FinSequence of the carrier of G by A34, FINSEQ_1:def_4;
set q = F2 |^ I2;
A38: len (F2 |^ I2) = len F2 by Def3;
then A39: dom (F2 |^ I2) = dom F2 by FINSEQ_3:29;
A40: dom F1 = dom I1 by A15, FINSEQ_3:29;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(F2_|^_I2)_holds_
((F2_|^_I2)_/._k)_"_=_(F1_|^_I1)_._(((len_(F1_|^_I1))_-_k)_+_1)
let k be Element of NAT ; ::_thesis: ( k in dom (F2 |^ I2) implies ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1) )
A41: I2 /. k = @ (I2 /. k) ;
assume A42: k in dom (F2 |^ I2) ; ::_thesis: ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1)
then reconsider n = ((len (F1 |^ I1)) - k) + 1 as Element of NAT by A17, A36, A38, Lm3;
A43: ( I1 /. n = @ (I1 /. n) & (F2 |^ I2) /. k = (F2 |^ I2) . k ) by A42, PARTFUN1:def_6;
 dom (F2 |^ I2) = dom I1 by A15, A17, A38, FINSEQ_3:29;
then consider i being Integer such that
A44: i = I1 . n and
A45: I2 . k = - i by A15, A29, A19, A36, A42;
 I2 . k = I2 /. k by A37, A39, A42, PARTFUN1:def_6;
then A46: (F2 |^ I2) . k = (F2 /. k) |^ (- i) by A39, A42, A45, A41, Def3;
A47: ( F2 /. k = F2 . k & F2 . k = F1 . n ) by A18, A36, A39, A42, PARTFUN1:def_6;
 ( 1 <= n & len (F1 |^ I1) >= n ) by A17, A36, A38, A42, Lm3;
then A48: n in dom I2 by A17, A30, A36, FINSEQ_3:25;
then A49: I1 . n = I1 /. n by A28, A19, PARTFUN1:def_6;
 F1 /. n = F1 . n by A15, A35, A28, A48, PARTFUN1:def_6;
then  (F2 |^ I2) . k = ((F1 /. n) |^ i) " by A46, A47, GROUP_1:36;
hence  ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1) by A40, A28, A19, A48, A44, A49, A43, Def3; ::_thesis: verum
end;
then  (Product (F1 |^ I1)) " = Product (F2 |^ I2) by A17, A36, A38, Th14;
hence  c " in B by A14, A30, A24; ::_thesis: verum
end;
A50: len {} = 0 ;
A51: ( rng (<*> the carrier of G) = {} & {} c= A ) by XBOOLE_1:2;
 ( 1_ G = Product (<*> the carrier of G) & (<*> the carrier of G) |^ (<*> INT) = {} ) by Th8, Th21;
then  1_ G in B by A51, A50;
then consider H being strict Subgroup of G such that
A52: the carrier of H = B by A2, A13, GROUP_2:52;
 A c= B
proof
reconsider p = 1 as Integer ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume A53: x in A ; ::_thesis: x in B
then reconsider a = x as Element of G ;
A54: ( rng <*a*> = {a} & {a} c= A ) by A53, FINSEQ_1:39, ZFMISC_1:31;
A55: ( len <*a*> = 1 & len <*(@ p)*> = 1 ) by FINSEQ_1:39;
Product (<*a*> |^ <*(@ p)*>) = Product <*(a |^ 1)*> by Th22
.= a |^ 1 by FINSOP_1:11
.= a by GROUP_1:26 ;
hence  x in B by A55, A54; ::_thesis: verum
end;
then  gr A is Subgroup of H by A52, Def4;
then  a in H by A1, GROUP_2:40;
then  a in B by A52, STRUCT_0:def_5;
then  ex b being Element of G st
( b = a & ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( b = Product (F |^ I) & len F = len I & rng F c= A ) ) ;
hence  ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) ; ::_thesis: verum
end;
given F being FinSequence of the carrier of G, I being FinSequence of INT  such that  len F = len I and
A56: rng F c= A and
A57: Product (F |^ I) = a ; ::_thesis: a in gr A
 A c= the carrier of (gr A) by Def4;
then  rng F c= carr (gr A) by A56, XBOOLE_1:1;
hence  a in gr A by A57, Th20; ::_thesis: verum
end;

theorem Th29: :: GROUP_4:29
for G being Group
for a being Element of G
for A being Subset of G st a in A holds
a in gr A
proof
let G be Group; ::_thesis: for a being Element of G
for A being Subset of G st a in A holds
a in gr A
let a be Element of G; ::_thesis: for A being Subset of G st a in A holds
a in gr A
let A be Subset of G; ::_thesis: ( a in A implies a in gr A )
assume A1: a in A ; ::_thesis: a in gr A
 A c= the carrier of (gr A) by Def4;
hence  a in gr A by A1, STRUCT_0:def_5; ::_thesis: verum
end;

theorem :: GROUP_4:30
for G being Group holds gr ({} the carrier of G) = (1). G
proof
let G be Group; ::_thesis: gr ({} the carrier of G) = (1). G
 ( {} the carrier of G c= the carrier of ((1). G) & ( for H being strict Subgroup of G st {} the carrier of G c= the carrier of H holds
(1). G is Subgroup of H ) ) by GROUP_2:65, XBOOLE_1:2;
hence  gr ({} the carrier of G) = (1). G by Def4; ::_thesis: verum
end;

theorem Th31: :: GROUP_4:31
for G being Group
for H being strict Subgroup of G holds gr (carr H) = H
proof
let G be Group; ::_thesis: for H being strict Subgroup of G holds gr (carr H) = H
let H be strict Subgroup of G; ::_thesis: gr (carr H) = H
 for H1 being strict Subgroup of G st carr H c= the carrier of H1 holds
H is Subgroup of H1 by GROUP_2:57;
hence  gr (carr H) = H by Def4; ::_thesis: verum
end;

theorem Th32: :: GROUP_4:32
for G being Group
for A, B being Subset of G st A c= B holds
gr A is Subgroup of gr B
proof
let G be Group; ::_thesis: for A, B being Subset of G st A c= B holds
gr A is Subgroup of gr B
let A, B be Subset of G; ::_thesis: ( A c= B implies gr A is Subgroup of gr B )
assume A1: A c= B ; ::_thesis: gr A is Subgroup of gr B
now__::_thesis:_for_a_being_Element_of_G_st_a_in_gr_A_holds_
a_in_gr_B
let a be Element of G; ::_thesis: ( a in gr A implies a in gr B )
assume  a in gr A ; ::_thesis: a in gr B
then consider F being FinSequence of the carrier of G, I being FinSequence of INT  such that
A2: len F = len I and
A3: rng F c= A and
A4: Product (F |^ I) = a by Th28;
 rng F c= B by A1, A3, XBOOLE_1:1;
hence  a in gr B by A2, A4, Th28; ::_thesis: verum
end;
hence  gr A is Subgroup of gr B by GROUP_2:58; ::_thesis: verum
end;

theorem :: GROUP_4:33
for G being Group
for A, B being Subset of G holds gr (A /\ B) is Subgroup of (gr A) /\ (gr B)
proof
let G be Group; ::_thesis: for A, B being Subset of G holds gr (A /\ B) is Subgroup of (gr A) /\ (gr B)
let A, B be Subset of G; ::_thesis: gr (A /\ B) is Subgroup of (gr A) /\ (gr B)
now__::_thesis:_for_a_being_Element_of_G_st_a_in_gr_(A_/\_B)_holds_
a_in_(gr_A)_/\_(gr_B)
let a be Element of G; ::_thesis: ( a in gr (A /\ B) implies a in (gr A) /\ (gr B) )
assume  a in gr (A /\ B) ; ::_thesis: a in (gr A) /\ (gr B)
then consider F being FinSequence of the carrier of G, I being FinSequence of INT  such that
A1: len F = len I and
A2: rng F c= A /\ B and
A3: Product (F |^ I) = a by Th28;
 A /\ B c= B by XBOOLE_1:17;
then  rng F c= B by A2, XBOOLE_1:1;
then A4: a in gr B by A1, A3, Th28;
 A /\ B c= A by XBOOLE_1:17;
then  rng F c= A by A2, XBOOLE_1:1;
then  a in gr A by A1, A3, Th28;
hence  a in (gr A) /\ (gr B) by A4, GROUP_2:82; ::_thesis: verum
end;
hence  gr (A /\ B) is Subgroup of (gr A) /\ (gr B) by GROUP_2:58; ::_thesis: verum
end;

theorem Th34: :: GROUP_4:34
for G being Group
for A being Subset of G holds the carrier of (gr A) = meet  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }
proof
let G be Group; ::_thesis: for A being Subset of G holds the carrier of (gr A) = meet  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }
let A be Subset of G; ::_thesis: the carrier of (gr A) = meet  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }
defpred S1[ Subgroup of G] means A c= carr $1;
set X =  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }  ;
A1: now__::_thesis:_for_Y_being_set_st_Y_in__{__B_where_B_is_Subset_of_G_:_ex_H_being_strict_Subgroup_of_G_st_
(_B_=_the_carrier_of_H_&_A_c=_carr_H_)__}__holds_
A_c=_Y
let Y be set ; ::_thesis: ( Y in  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }  implies A c= Y )
assume  Y in  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }  ; ::_thesis: A c= Y
then  ex B being Subset of G st
( Y = B & ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H ) ) ;
hence  A c= Y ; ::_thesis: verum
end;
 the carrier of ((Omega). G) = carr ((Omega). G) ;
then A2: ex H being strict Subgroup of G st S1[H] ;
consider H being strict Subgroup of G such that
A3: the carrier of H = meet  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S1[H] )  }  from GROUP_4:sch_1(A2);
A4: now__::_thesis:_for_H1_being_strict_Subgroup_of_G_st_A_c=_the_carrier_of_H1_holds_
H_is_Subgroup_of_H1
let H1 be strict Subgroup of G; ::_thesis: ( A c= the carrier of H1 implies H is Subgroup of H1 )
A5: the carrier of H1 = carr H1 ;
assume  A c= the carrier of H1 ; ::_thesis: H is Subgroup of H1
then  the carrier of H1 in  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }  by A5;
hence  H is Subgroup of H1 by A3, GROUP_2:57, SETFAM_1:3; ::_thesis: verum
end;
 carr ((Omega). G) in  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }  ;
then  A c= the carrier of H by A3, A1, SETFAM_1:5;
hence  the carrier of (gr A) = meet  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }  by A3, A4, Def4; ::_thesis: verum
end;

theorem Th35: :: GROUP_4:35
for G being Group
for A being Subset of G holds gr A = gr (A \ {(1_ G)})
proof
let G be Group; ::_thesis: for A being Subset of G holds gr A = gr (A \ {(1_ G)})
let A be Subset of G; ::_thesis: gr A = gr (A \ {(1_ G)})
set X =  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }  ;
set Y =  {  C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H )  }  ;
A1:  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }  =  {  C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H )  }
proof
thus   {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }  c=  {  C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H )  }  c=  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }  or x in  {  C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H )  }  )
assume  x in  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }  ; ::_thesis: x in  {  C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H )  }
then consider B being Subset of G such that
A2: x = B and
A3: ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H ) ;
consider H being strict Subgroup of G such that
A4: B = the carrier of H and
A5: A c= carr H by A3;
 A \ {(1_ G)} c= A by XBOOLE_1:36;
then  A \ {(1_ G)} c= carr H by A5, XBOOLE_1:1;
hence  x in  {  C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H )  }  by A2, A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H )  }  or x in  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }  )
assume  x in  {  C where C is Subset of G : ex H being strict Subgroup of G st
( C = the carrier of H & A \ {(1_ G)} c= carr H )  }  ; ::_thesis: x in  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }
then consider B being Subset of G such that
A6: x = B and
A7: ex H being strict Subgroup of G st
( B = the carrier of H & A \ {(1_ G)} c= carr H ) ;
consider H being strict Subgroup of G such that
A8: B = the carrier of H and
A9: A \ {(1_ G)} c= carr H by A7;
 1_ G in H by GROUP_2:46;
then  1_ G in carr H by STRUCT_0:def_5;
then  {(1_ G)} c= carr H by ZFMISC_1:31;
then A10: (A \ {(1_ G)}) \/ {(1_ G)} c= carr H by A9, XBOOLE_1:8;
now__::_thesis:_A_c=_carr_H
percases ( 1_ G in A or not 1_ G in A ) ;
suppose 1_ G in A ; ::_thesis: A c= carr H
then  {(1_ G)} c= A by ZFMISC_1:31;
hence  A c= carr H by A10, XBOOLE_1:45; ::_thesis: verum
end;
suppose not 1_ G in A ; ::_thesis: A c= carr H
hence  A c= carr H by A9, ZFMISC_1:57; ::_thesis: verum
end;
end;
end;
hence  x in  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }  by A6, A8; ::_thesis: verum
end;
the carrier of (gr A) = meet  {  B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & A c= carr H )  }  by Th34
.= the carrier of (gr (A \ {(1_ G)})) by A1, Th34 ;
hence  gr A = gr (A \ {(1_ G)}) by GROUP_2:59; ::_thesis: verum
end;

definition
let G be Group;
let a be Element of G;
attra is generating  means :Def5: :: GROUP_4:def 5
 ex A being Subset of G st
( gr A = multMagma(# the carrier of G, the multF of G #) & not gr (A \ {a}) = multMagma(# the carrier of G, the multF of G #) );
end;

:: deftheorem Def5 defines generating GROUP_4:def_5_:_
 for G being Group
for a being Element of G holds
( a is generating iff ex A being Subset of G st
( gr A = multMagma(# the carrier of G, the multF of G #) & not gr (A \ {a}) = multMagma(# the carrier of G, the multF of G #) ) );

theorem :: GROUP_4:36
for G being Group holds not 1_ G is generating
proof
let G be Group; ::_thesis: not 1_ G is generating
let A be Subset of G; :: according to GROUP_4:def_5 ::_thesis: ( gr A = multMagma(# the carrier of G, the multF of G #) implies gr (A \ {(1_ G)}) = multMagma(# the carrier of G, the multF of G #) )
assume  gr A = multMagma(# the carrier of G, the multF of G #) ; ::_thesis: gr (A \ {(1_ G)}) = multMagma(# the carrier of G, the multF of G #)
hence  gr (A \ {(1_ G)}) = multMagma(# the carrier of G, the multF of G #) by Th35; ::_thesis: verum
end;

definition
let G be Group;
let H be Subgroup of G;
attrH is maximal  means :Def6: :: GROUP_4:def 6
( multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of G, the multF of G #) & ( for K being strict Subgroup of G st multMagma(# the carrier of H, the multF of H #) <> K & H is Subgroup of K holds
K = multMagma(# the carrier of G, the multF of G #) ) );
end;

:: deftheorem Def6 defines maximal GROUP_4:def_6_:_
 for G being Group
for H being Subgroup of G holds
( H is maximal iff ( multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of G, the multF of G #) & ( for K being strict Subgroup of G st multMagma(# the carrier of H, the multF of H #) <> K & H is Subgroup of K holds
K = multMagma(# the carrier of G, the multF of G #) ) ) );

theorem Th37: :: GROUP_4:37
for G being strict Group
for H being strict Subgroup of G
for a being Element of G st H is maximal & not a in H holds
gr ((carr H) \/ {a}) = G
proof
let G be strict Group; ::_thesis: for H being strict Subgroup of G
for a being Element of G st H is maximal & not a in H holds
gr ((carr H) \/ {a}) = G
let H be strict Subgroup of G; ::_thesis: for a being Element of G st H is maximal & not a in H holds
gr ((carr H) \/ {a}) = G
let a be Element of G; ::_thesis: ( H is maximal & not a in H implies gr ((carr H) \/ {a}) = G )
assume that
A1: H is maximal and
A2: not a in H ; ::_thesis: gr ((carr H) \/ {a}) = G
 gr (carr H) is Subgroup of gr ((carr H) \/ {a}) by Th32, XBOOLE_1:7;
then A3: H is Subgroup of gr ((carr H) \/ {a}) by Th31;
 a in {a} by TARSKI:def_1;
then  a in (carr H) \/ {a} by XBOOLE_0:def_3;
then  H <> gr ((carr H) \/ {a}) by A2, Th29;
hence  gr ((carr H) \/ {a}) = G by A1, A3, Def6; ::_thesis: verum
end;

definition
let G be Group;
func Phi G ->  strict Subgroup of G means :Def7: :: GROUP_4:def 7
 the carrier of it = meet  {  A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal )  }   if  ex H being strict Subgroup of G st H is maximal
otherwise it = multMagma(# the carrier of G, the multF of G #);
existence
 ( ( ex H being strict Subgroup of G st H is maximal implies ex b1 being strict Subgroup of G st the carrier of b1 = meet  {  A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal )  }  ) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ex b1 being strict Subgroup of G st b1 = multMagma(# the carrier of G, the multF of G #) ) )
proof
defpred S1[ Subgroup of G] means $1 is maximal ;
now__::_thesis:_(_(_ex_H_being_strict_Subgroup_of_G_st_H_is_maximal_implies_ex_b1_being_strict_Subgroup_of_G_st_the_carrier_of_b1_=_meet__{__A_where_A_is_Subset_of_G_:_ex_H_being_strict_Subgroup_of_G_st_
(_A_=_the_carrier_of_H_&_H_is_maximal_)__}__)_&_(_(_for_H_being_strict_Subgroup_of_G_holds_not_H_is_maximal_)_implies_ex_b1_being_strict_Subgroup_of_G_st_b1_=_multMagma(#_the_carrier_of_G,_the_multF_of_G_#)_)_)
percases ( ex H being strict Subgroup of G st S1[H] or for H being strict Subgroup of G holds not H is maximal ) ;
supposeA1: ex H being strict Subgroup of G st S1[H] ; ::_thesis: ( ( ex H being strict Subgroup of G st H is maximal implies ex b1 being strict Subgroup of G st the carrier of b1 = meet  {  A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal )  }  ) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ex b1 being strict Subgroup of G st b1 = multMagma(# the carrier of G, the multF of G #) ) )
 ex H being strict Subgroup of G st the carrier of H = meet  {  A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & S1[K] )  }  from GROUP_4:sch_1(A1);
hence  ( ( ex H being strict Subgroup of G st H is maximal implies ex b1 being strict Subgroup of G st the carrier of b1 = meet  {  A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal )  }  ) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ex b1 being strict Subgroup of G st b1 = multMagma(# the carrier of G, the multF of G #) ) ) by A1; ::_thesis: verum
end;
supposeA2: for H being strict Subgroup of G holds not H is maximal ; ::_thesis: ( ( ex H being strict Subgroup of G st H is maximal implies ex b1 being strict Subgroup of G st the carrier of b1 = meet  {  A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal )  }  ) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ex b1 being strict Subgroup of G st b1 = multMagma(# the carrier of G, the multF of G #) ) )
 (Omega). G = multMagma(# the carrier of G, the multF of G #) ;
hence  ( ( ex H being strict Subgroup of G st H is maximal implies ex b1 being strict Subgroup of G st the carrier of b1 = meet  {  A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal )  }  ) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ex b1 being strict Subgroup of G st b1 = multMagma(# the carrier of G, the multF of G #) ) ) by A2; ::_thesis: verum
end;
end;
end;
hence  ( ( ex H being strict Subgroup of G st H is maximal implies ex b1 being strict Subgroup of G st the carrier of b1 = meet  {  A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal )  }  ) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ex b1 being strict Subgroup of G st b1 = multMagma(# the carrier of G, the multF of G #) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Subgroup of G holds
( ( ex H being strict Subgroup of G st H is maximal & the carrier of b1 = meet  {  A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal )  }  & the carrier of b2 = meet  {  A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal )  }  implies b1 = b2 ) & ( ( for H being strict Subgroup of G holds not H is maximal ) & b1 = multMagma(# the carrier of G, the multF of G #) & b2 = multMagma(# the carrier of G, the multF of G #) implies b1 = b2 ) ) by GROUP_2:59;
correctness
consistency
for b1 being strict Subgroup of G holds verum;
;
end;

:: deftheorem Def7 defines Phi GROUP_4:def_7_:_
 for G being Group
for b2 being strict Subgroup of G holds
( ( ex H being strict Subgroup of G st H is maximal implies ( b2 = Phi G iff the carrier of b2 = meet  {  A where A is Subset of G : ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal )  }  ) ) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ( b2 = Phi G iff b2 = multMagma(# the carrier of G, the multF of G #) ) ) );

theorem Th38: :: GROUP_4:38
for G being Group
for a being Element of G
for G being Group st ex H being strict Subgroup of G st H is maximal holds
( a in Phi G iff for H being strict Subgroup of G st H is maximal holds
a in H )
proof
let G be Group; ::_thesis: for a being Element of G
for G being Group st ex H being strict Subgroup of G st H is maximal holds
( a in Phi G iff for H being strict Subgroup of G st H is maximal holds
a in H )
let a be Element of G; ::_thesis: for G being Group st ex H being strict Subgroup of G st H is maximal holds
( a in Phi G iff for H being strict Subgroup of G st H is maximal holds
a in H )
let G be Group; ::_thesis: ( ex H being strict Subgroup of G st H is maximal implies ( a in Phi G iff for H being strict Subgroup of G st H is maximal holds
a in H ) )
set X =  {  A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & K is maximal )  }  ;
assume A1: ex H being strict Subgroup of G st H is maximal ; ::_thesis: ( a in Phi G iff for H being strict Subgroup of G st H is maximal holds
a in H )
then consider H being strict Subgroup of G such that
A2: H is maximal ;
thus  ( a in Phi G implies for H being strict Subgroup of G st H is maximal holds
a in H ) ::_thesis: ( ( for H being strict Subgroup of G st H is maximal holds
a in H ) implies a in Phi G )
proof
assume  a in Phi G ; ::_thesis: for H being strict Subgroup of G st H is maximal holds
a in H
then  a in the carrier of (Phi G) by STRUCT_0:def_5;
then A3: a in meet  {  A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & K is maximal )  }  by A1, Def7;
let H be strict Subgroup of G; ::_thesis: ( H is maximal implies a in H )
assume  H is maximal ; ::_thesis: a in H
then  carr H in  {  A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & K is maximal )  }  ;
then  a in carr H by A3, SETFAM_1:def_1;
hence  a in H by STRUCT_0:def_5; ::_thesis: verum
end;
assume A4: for H being strict Subgroup of G st H is maximal holds
a in H ; ::_thesis: a in Phi G
A5: now__::_thesis:_for_Y_being_set_st_Y_in__{__A_where_A_is_Subset_of_G_:_ex_K_being_strict_Subgroup_of_G_st_
(_A_=_the_carrier_of_K_&_K_is_maximal_)__}__holds_
a_in_Y
let Y be set ; ::_thesis: ( Y in  {  A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & K is maximal )  }  implies a in Y )
assume  Y in  {  A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & K is maximal )  }  ; ::_thesis: a in Y
then consider A being Subset of G such that
A6: Y = A and
A7: ex H being strict Subgroup of G st
( A = the carrier of H & H is maximal ) ;
consider H being strict Subgroup of G such that
A8: A = the carrier of H and
A9: H is maximal by A7;
 a in H by A4, A9;
hence  a in Y by A6, A8, STRUCT_0:def_5; ::_thesis: verum
end;
 carr H in  {  A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & K is maximal )  }  by A2;
then  a in meet  {  A where A is Subset of G : ex K being strict Subgroup of G st
( A = the carrier of K & K is maximal )  }  by A5, SETFAM_1:def_1;
then  a in the carrier of (Phi G) by A1, Def7;
hence  a in Phi G by STRUCT_0:def_5; ::_thesis: verum
end;

theorem :: GROUP_4:39
for G being Group
for a being Element of G st ( for H being strict Subgroup of G holds not H is maximal ) holds
a in Phi G
proof
let G be Group; ::_thesis: for a being Element of G st ( for H being strict Subgroup of G holds not H is maximal ) holds
a in Phi G
let a be Element of G; ::_thesis: ( ( for H being strict Subgroup of G holds not H is maximal ) implies a in Phi G )
assume  for H being strict Subgroup of G holds not H is maximal ; ::_thesis: a in Phi G
then  Phi G = multMagma(# the carrier of G, the multF of G #) by Def7;
hence  a in Phi G by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th40: :: GROUP_4:40
for G being Group
for H being strict Subgroup of G st H is maximal holds
Phi G is Subgroup of H
proof
let G be Group; ::_thesis: for H being strict Subgroup of G st H is maximal holds
Phi G is Subgroup of H
let H be strict Subgroup of G; ::_thesis: ( H is maximal implies Phi G is Subgroup of H )
assume  H is maximal ; ::_thesis: Phi G is Subgroup of H
then  for a being Element of G st a in Phi G holds
a in H by Th38;
hence  Phi G is Subgroup of H by GROUP_2:58; ::_thesis: verum
end;

theorem Th41: :: GROUP_4:41
for G being strict Group holds the carrier of (Phi G) =  {  a where a is Element of G : not a is generating  }
proof
let G be strict Group; ::_thesis: the carrier of (Phi G) =  {  a where a is Element of G : not a is generating  }
set A =  {  a where a is Element of G : not a is generating  }  ;
thus  the carrier of (Phi G) c=  {  a where a is Element of G : not a is generating  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  a where a is Element of G : not a is generating  }  c= the carrier of (Phi G)
proof
defpred S1[ set , set ] means  ex H1, H2 being strict Subgroup of G st
( $1 = H1 & $2 = H2 & H1 is Subgroup of H2 );
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (Phi G) or x in  {  a where a is Element of G : not a is generating  }  )
assume A1: x in the carrier of (Phi G) ; ::_thesis: x in  {  a where a is Element of G : not a is generating  }
then  x in Phi G by STRUCT_0:def_5;
then  x in G by GROUP_2:40;
then reconsider a = x as Element of G by STRUCT_0:def_5;
assume  not x in  {  a where a is Element of G : not a is generating  }  ; ::_thesis: contradiction
then  a is generating ;
then consider B being Subset of G such that
A2: gr B = G and
A3: gr (B \ {a}) <> G by Def5;
set M = B \ {a};
A4: now__::_thesis:_not_a_in_gr_(B_\_{a})
assume A5: a in gr (B \ {a}) ; ::_thesis: contradiction
now__::_thesis:_for_b_being_Element_of_G_holds_b_in_gr_(B_\_{a})
let b be Element of G; ::_thesis: b in gr (B \ {a})
 b in gr B by A2, STRUCT_0:def_5;
then consider F being FinSequence of the carrier of G, I being FinSequence of INT  such that
 len I = len F and
A6: rng F c= B and
A7: b = Product (F |^ I) by Th28;
 rng (F |^ I) c= carr (gr (B \ {a}))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (F |^ I) or x in carr (gr (B \ {a})) )
assume  x in rng (F |^ I) ; ::_thesis: x in carr (gr (B \ {a}))
then consider y being set  such that
A8: y in dom (F |^ I) and
A9: (F |^ I) . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A8;
 len (F |^ I) = len F by Def3;
then A10: y in dom F by A8, FINSEQ_3:29;
then A11: x = (F /. y) |^ (@ (I /. y)) by A9, Def3;
now__::_thesis:_x_in_carr_(gr_(B_\_{a}))
percases ( F /. y = a or F /. y <> a ) ;
suppose F /. y = a ; ::_thesis: x in carr (gr (B \ {a}))
then  x in gr (B \ {a}) by A5, A11, Th4;
hence  x in carr (gr (B \ {a})) by STRUCT_0:def_5; ::_thesis: verum
end;
suppose F /. y <> a ; ::_thesis: x in carr (gr (B \ {a}))
then A12: not F /. y in {a} by TARSKI:def_1;
 ( F /. y = F . y & F . y in rng F ) by A10, FUNCT_1:def_3, PARTFUN1:def_6;
then  F /. y in B \ {a} by A6, A12, XBOOLE_0:def_5;
then  x in gr (B \ {a}) by A11, Th4, Th29;
hence  x in carr (gr (B \ {a})) by STRUCT_0:def_5; ::_thesis: verum
end;
end;
end;
hence  x in carr (gr (B \ {a})) ; ::_thesis: verum
end;
hence  b in gr (B \ {a}) by A7, Th18; ::_thesis: verum
end;
hence  contradiction by A3, GROUP_2:62; ::_thesis: verum
end;
defpred S2[ Subgroup of G] means ( B \ {a} c= carr $1 & not a in $1 );
consider X being set  such that
A13: X c= Subgroups G and
A14: for H being strict Subgroup of G holds
( H in X iff S2[H] ) from GROUP_4:sch_2();
 B \ {a} c= carr (gr (B \ {a})) by Def4;
then reconsider X = X as non empty set by A14, A4;
A15: for x, y, z being Element of X st S1[x,y] & S1[y,z] holds
S1[x,z]
proof
let x, y, z be Element of X; ::_thesis: ( S1[x,y] & S1[y,z] implies S1[x,z] )
given H1, H2 being strict Subgroup of G such that A16: x = H1 and
A17: ( y = H2 & H1 is Subgroup of H2 ) ; ::_thesis: ( not S1[y,z] or S1[x,z] )
given H3, H4 being strict Subgroup of G such that A18: y = H3 and
A19: z = H4 and
A20: H3 is Subgroup of H4 ; ::_thesis: S1[x,z]
 H1 is Subgroup of H4 by A17, A18, A20, GROUP_2:56;
hence  S1[x,z] by A16, A19; ::_thesis: verum
end;
A21: for Y being set st Y c= X & ( for x, y being Element of X st x in Y & y in Y & not S1[x,y] holds
S1[y,x] ) holds
ex y being Element of X st
for x being Element of X st x in Y holds
S1[x,y]
proof
let Y be set ; ::_thesis: ( Y c= X & ( for x, y being Element of X st x in Y & y in Y & not S1[x,y] holds
S1[y,x] ) implies ex y being Element of X st
for x being Element of X st x in Y holds
S1[x,y] )
assume A22: Y c= X ; ::_thesis: ( ex x, y being Element of X st
( x in Y & y in Y & not S1[x,y] & not S1[y,x] ) or ex y being Element of X st
for x being Element of X st x in Y holds
S1[x,y] )
set C =  {  D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H )  }  ;
now__::_thesis:_for_Z_being_set_st_Z_in__{__D_where_D_is_Subset_of_G_:_ex_H_being_strict_Subgroup_of_G_st_
(_H_in_Y_&_D_=_carr_H_)__}__holds_
Z_c=_the_carrier_of_G
let Z be set ; ::_thesis: ( Z in  {  D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H )  }  implies Z c= the carrier of G )
assume  Z in  {  D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H )  }  ; ::_thesis: Z c= the carrier of G
then  ex D being Subset of G st
( Z = D & ex H being strict Subgroup of G st
( H in Y & D = carr H ) ) ;
hence  Z c= the carrier of G ; ::_thesis: verum
end;
then reconsider E = union  {  D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H )  }  as Subset of G by ZFMISC_1:76;
assume A23: for x, y being Element of X st x in Y & y in Y & not S1[x,y] holds
S1[y,x] ; ::_thesis: ex y being Element of X st
for x being Element of X st x in Y holds
S1[x,y]
now__::_thesis:_ex_y_being_Element_of_X_st_
for_x_being_Element_of_X_st_x_in_Y_holds_
S1[x,y]
percases ( Y = {} or Y <> {} ) ;
supposeA24: Y = {} ; ::_thesis: ex y being Element of X st
for x being Element of X st x in Y holds
S1[x,y]
set y = the Element of X;
take y = the Element of X; ::_thesis: for x being Element of X st x in Y holds
S1[x,y]
let x be Element of X; ::_thesis: ( x in Y implies S1[x,y] )
assume  x in Y ; ::_thesis: S1[x,y]
hence  S1[x,y] by A24; ::_thesis: verum
end;
supposeA25: Y <> {} ; ::_thesis: ex y being Element of X st
for x being Element of X st x in Y holds
ex K, H being strict Subgroup of G st
( x = K & y = H & K is Subgroup of H )
A26: now__::_thesis:_for_a,_b_being_Element_of_G_st_a_in_E_&_b_in_E_holds_
a_*_b_in_E
let a, b be Element of G; ::_thesis: ( a in E & b in E implies a * b in E )
assume that
A27: a in E and
A28: b in E ; ::_thesis: a * b in E
consider Z being set  such that
A29: a in Z and
A30: Z in  {  D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H )  }  by A27, TARSKI:def_4;
consider Z1 being set  such that
A31: b in Z1 and
A32: Z1 in  {  D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H )  }  by A28, TARSKI:def_4;
consider D being Subset of G such that
A33: Z = D and
A34: ex H being strict Subgroup of G st
( H in Y & D = carr H ) by A30;
consider B being Subset of G such that
A35: Z1 = B and
A36: ex H being strict Subgroup of G st
( H in Y & B = carr H ) by A32;
consider H1 being Subgroup of G such that
A37: H1 in Y and
A38: D = carr H1 by A34;
consider H2 being Subgroup of G such that
A39: H2 in Y and
A40: B = carr H2 by A36;
now__::_thesis:_a_*_b_in_E
percases ( S1[H1,H2] or S1[H2,H1] ) by A22, A23, A37, A39;
suppose S1[H1,H2] ; ::_thesis: a * b in E
then  carr H1 c= the carrier of H2 by GROUP_2:def_5;
then  a * b in carr H2 by A29, A33, A38, A31, A35, A40, GROUP_2:74;
hence  a * b in E by A32, A35, A40, TARSKI:def_4; ::_thesis: verum
end;
suppose S1[H2,H1] ; ::_thesis: a * b in E
then  carr H2 c= the carrier of H1 by GROUP_2:def_5;
then  a * b in carr H1 by A29, A33, A38, A31, A35, A40, GROUP_2:74;
hence  a * b in E by A30, A33, A38, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence  a * b in E ; ::_thesis: verum
end;
A41: now__::_thesis:_for_a_being_Element_of_G_st_a_in_E_holds_
a_"_in_E
let a be Element of G; ::_thesis: ( a in E implies a " in E )
assume  a in E ; ::_thesis: a " in E
then consider Z being set  such that
A42: a in Z and
A43: Z in  {  D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H )  }  by TARSKI:def_4;
consider D being Subset of G such that
A44: Z = D and
A45: ex H being strict Subgroup of G st
( H in Y & D = carr H ) by A43;
consider H1 being Subgroup of G such that
 H1 in Y and
A46: D = carr H1 by A45;
 a " in carr H1 by A42, A44, A46, GROUP_2:75;
hence  a " in E by A43, A44, A46, TARSKI:def_4; ::_thesis: verum
end;
set s = the Element of Y;
A47: the Element of Y in X by A22, A25, TARSKI:def_3;
then reconsider s = the Element of Y as strict Subgroup of G by A13, GROUP_3:def_1;
A48: carr s in  {  D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H )  }  by A25;
then A49: carr s c= E by ZFMISC_1:74;
 E <> {} by A48, ORDERS_1:6;
then consider H being strict Subgroup of G such that
A50: the carrier of H = E by A26, A41, GROUP_2:52;
A51: now__::_thesis:_not_a_in_H
assume  a in H ; ::_thesis: contradiction
then  a in E by A50, STRUCT_0:def_5;
then consider Z being set  such that
A52: a in Z and
A53: Z in  {  D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H )  }  by TARSKI:def_4;
consider D being Subset of G such that
A54: Z = D and
A55: ex H being strict Subgroup of G st
( H in Y & D = carr H ) by A53;
consider H1 being strict Subgroup of G such that
A56: H1 in Y and
A57: D = carr H1 by A55;
 not a in H1 by A14, A22, A56;
hence  contradiction by A52, A54, A57, STRUCT_0:def_5; ::_thesis: verum
end;
 B \ {a} c= carr s by A14, A47;
then A58: B \ {a} c= E by A49, XBOOLE_1:1;
 the carrier of H = carr H ;
then reconsider y = H as Element of X by A14, A58, A50, A51;
take y = y; ::_thesis: for x being Element of X st x in Y holds
ex K, H being strict Subgroup of G st
( x = K & y = H & K is Subgroup of H )
let x be Element of X; ::_thesis: ( x in Y implies ex K, H being strict Subgroup of G st
( x = K & y = H & K is Subgroup of H ) )
assume A59: x in Y ; ::_thesis: ex K, H being strict Subgroup of G st
( x = K & y = H & K is Subgroup of H )
 x in Subgroups G by A13, TARSKI:def_3;
then reconsider K = x as strict Subgroup of G by GROUP_3:def_1;
take K = K; ::_thesis: ex H being strict Subgroup of G st
( x = K & y = H & K is Subgroup of H )
take H = H; ::_thesis: ( x = K & y = H & K is Subgroup of H )
thus  ( x = K & y = H ) ; ::_thesis: K is Subgroup of H
 carr K = the carrier of K ;
then  the carrier of K in  {  D where D is Subset of G : ex H being strict Subgroup of G st
( H in Y & D = carr H )  }  by A59;
hence  K is Subgroup of H by A50, GROUP_2:57, ZFMISC_1:74; ::_thesis: verum
end;
end;
end;
hence  ex y being Element of X st
for x being Element of X st x in Y holds
S1[x,y] ; ::_thesis: verum
end;
A60: now__::_thesis:_for_x_being_Element_of_X_holds_x_is_strict_Subgroup_of_G
let x be Element of X; ::_thesis: x is strict Subgroup of G
 x in Subgroups G by A13, TARSKI:def_3;
hence  x is strict Subgroup of G by GROUP_3:def_1; ::_thesis: verum
end;
A61: for x being Element of X holds S1[x,x]
proof
let x be Element of X; ::_thesis: S1[x,x]
reconsider H = x as strict Subgroup of G by A60;
 H is Subgroup of H by GROUP_2:54;
hence  S1[x,x] ; ::_thesis: verum
end;
A62: for x, y being Element of X st S1[x,y] & S1[y,x] holds
x = y by GROUP_2:55;
consider s being Element of X such that
A63: for y being Element of X st s <> y holds
not S1[s,y] from ORDERS_1:sch_1(A61, A62, A15, A21);
reconsider H = s as strict Subgroup of G by A60;
 H is maximal
proof
 not a in H by A14;
hence  multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of G, the multF of G #) by STRUCT_0:def_5; :: according to GROUP_4:def_6 ::_thesis: for K being strict Subgroup of G st multMagma(# the carrier of H, the multF of H #) <> K & H is Subgroup of K holds
K = multMagma(# the carrier of G, the multF of G #)
let K be strict Subgroup of G; ::_thesis: ( multMagma(# the carrier of H, the multF of H #) <> K & H is Subgroup of K implies K = multMagma(# the carrier of G, the multF of G #) )
assume that
A64: K <> multMagma(# the carrier of H, the multF of H #) and
A65: H is Subgroup of K and
A66: K <> multMagma(# the carrier of G, the multF of G #) ; ::_thesis: contradiction
A67: B \ {a} c= carr H by A14;
 the carrier of H c= the carrier of K by A65, GROUP_2:def_5;
then A68: B \ {a} c= carr K by A67, XBOOLE_1:1;
now__::_thesis:_not_a_in_K
A69: B c= (B \ {a}) \/ {a}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in (B \ {a}) \/ {a} )
assume A70: x in B ; ::_thesis: x in (B \ {a}) \/ {a}
now__::_thesis:_x_in_(B_\_{a})_\/_{a}
percases ( x = a or x <> a ) ;
suppose x = a ; ::_thesis: x in (B \ {a}) \/ {a}
then  x in {a} by TARSKI:def_1;
hence  x in (B \ {a}) \/ {a} by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x <> a ; ::_thesis: x in (B \ {a}) \/ {a}
then  not x in {a} by TARSKI:def_1;
then  x in B \ {a} by A70, XBOOLE_0:def_5;
hence  x in (B \ {a}) \/ {a} by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  x in (B \ {a}) \/ {a} ; ::_thesis: verum
end;
assume  a in K ; ::_thesis: contradiction
then  a in carr K by STRUCT_0:def_5;
then  {a} c= carr K by ZFMISC_1:31;
then  (B \ {a}) \/ {a} c= carr K by A68, XBOOLE_1:8;
then  gr B is Subgroup of gr (carr K) by A69, Th32, XBOOLE_1:1;
then  G is Subgroup of K by A2, Th31;
hence  contradiction by A66, GROUP_2:55; ::_thesis: verum
end;
then reconsider v = K as Element of X by A14, A68;
 not S1[s,v] by A63, A64;
hence  contradiction by A65; ::_thesis: verum
end;
then  Phi G is Subgroup of H by Th40;
then  the carrier of (Phi G) c= the carrier of H by GROUP_2:def_5;
then  x in H by A1, STRUCT_0:def_5;
hence  contradiction by A14; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  a where a is Element of G : not a is generating  }  or x in the carrier of (Phi G) )
assume  x in  {  a where a is Element of G : not a is generating  }  ; ::_thesis: x in the carrier of (Phi G)
then consider a being Element of G such that
A71: x = a and
A72: not a is generating ;
now__::_thesis:_x_in_the_carrier_of_(Phi_G)
percases ( for H being strict Subgroup of G holds not H is maximal or ex H being strict Subgroup of G st H is maximal ) ;
suppose for H being strict Subgroup of G holds not H is maximal ; ::_thesis: x in the carrier of (Phi G)
then  Phi G = G by Def7;
hence  x in the carrier of (Phi G) by A71; ::_thesis: verum
end;
supposeA73: ex H being strict Subgroup of G st H is maximal ; ::_thesis: x in the carrier of (Phi G)
now__::_thesis:_for_H_being_strict_Subgroup_of_G_st_H_is_maximal_holds_
a_in_H
let H be strict Subgroup of G; ::_thesis: ( H is maximal implies a in H )
assume A74: H is maximal ; ::_thesis: a in H
now__::_thesis:_a_in_H
assume A75: not a in H ; ::_thesis: contradiction
 (carr H) /\ {a} c= {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (carr H) /\ {a} or x in {} )
assume A76: x in (carr H) /\ {a} ; ::_thesis: x in {}
then  x in {a} by XBOOLE_0:def_4;
then A77: x = a by TARSKI:def_1;
 x in carr H by A76, XBOOLE_0:def_4;
hence  x in {} by A75, A77, STRUCT_0:def_5; ::_thesis: verum
end;
then  (carr H) /\ {a} = {} ;
then A78: carr H misses {a} by XBOOLE_0:def_7;
((carr H) \/ {a}) \ {a} = (carr H) \ {a} by XBOOLE_1:40
.= carr H by A78, XBOOLE_1:83 ;
then A79: gr (((carr H) \/ {a}) \ {a}) = H by Th31;
A80: H <> G by A74, Def6;
 gr ((carr H) \/ {a}) = G by A74, A75, Th37;
hence  contradiction by A72, A79, A80, Def5; ::_thesis: verum
end;
hence  a in H ; ::_thesis: verum
end;
then  a in Phi G by A73, Th38;
hence  x in the carrier of (Phi G) by A71, STRUCT_0:def_5; ::_thesis: verum
end;
end;
end;
hence  x in the carrier of (Phi G) ; ::_thesis: verum
end;

theorem :: GROUP_4:42
for G being strict Group
for a being Element of G holds
( a in Phi G iff not a is generating )
proof
let G be strict Group; ::_thesis: for a being Element of G holds
( a in Phi G iff not a is generating )
let a be Element of G; ::_thesis: ( a in Phi G iff not a is generating )
thus  ( a in Phi G implies not a is generating ) ::_thesis: ( not a is generating implies a in Phi G )
proof
assume  a in Phi G ; ::_thesis: not a is generating
then  a in the carrier of (Phi G) by STRUCT_0:def_5;
then  a in  {  b where b is Element of G : not b is generating  }  by Th41;
then  ex b being Element of G st
( a = b & not b is generating ) ;
hence  not a is generating ; ::_thesis: verum
end;
assume  not a is generating ; ::_thesis: a in Phi G
then  a in  {  b where b is Element of G : not b is generating  }  ;
then  a in the carrier of (Phi G) by Th41;
hence  a in Phi G by STRUCT_0:def_5; ::_thesis: verum
end;

definition
let G be Group;
let H1, H2 be Subgroup of G;
funcH1 * H2 ->  Subset of G equals :: GROUP_4:def 8
(carr H1) * (carr H2);
correctness
coherence
(carr H1) * (carr H2) is Subset of G;
;
end;

:: deftheorem  defines * GROUP_4:def_8_:_
 for G being Group
for H1, H2 being Subgroup of G holds H1 * H2 = (carr H1) * (carr H2);

theorem :: GROUP_4:43
for G being Group
for H1, H2 being Subgroup of G holds
( H1 * H2 = (carr H1) * (carr H2) & H1 * H2 = H1 * (carr H2) & H1 * H2 = (carr H1) * H2 ) ;

theorem :: GROUP_4:44
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)
thus (H1 * H2) * H3 = (carr H1) * ((carr H2) * H3) by GROUP_2:96
.= H1 * (H2 * H3) ; ::_thesis: verum
end;

theorem :: GROUP_4:45
for G being Group
for a being Element of G
for H1, H2 being Subgroup of G holds (a * H1) * H2 = a * (H1 * 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 * H2)
let a be Element of G; ::_thesis: for H1, H2 being Subgroup of G holds (a * H1) * H2 = a * (H1 * H2)
let H1, H2 be Subgroup of G; ::_thesis: (a * H1) * H2 = a * (H1 * H2)
thus (a * H1) * H2 = a * ((carr H1) * H2) by GROUP_2:96
.= a * (H1 * H2) ; ::_thesis: verum
end;

theorem :: GROUP_4:46
for G being Group
for a being Element of G
for H1, H2 being Subgroup of G holds (H1 * H2) * a = H1 * (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 * (H2 * a)
let a be Element of G; ::_thesis: for H1, H2 being Subgroup of G holds (H1 * H2) * a = H1 * (H2 * a)
let H1, H2 be Subgroup of G; ::_thesis: (H1 * H2) * a = H1 * (H2 * a)
thus (H1 * H2) * a = (H1 * (carr H2)) * a
.= H1 * (H2 * a) by GROUP_2:98 ; ::_thesis: verum
end;

theorem :: GROUP_4:47
for G being Group
for A being Subset of G
for H1, H2 being Subgroup of G holds (A * H1) * H2 = A * (H1 * H2)
proof
let G be Group; ::_thesis: for A being Subset of G
for H1, H2 being Subgroup of G holds (A * H1) * H2 = A * (H1 * H2)
let A be Subset of G; ::_thesis: for H1, H2 being Subgroup of G holds (A * H1) * H2 = A * (H1 * H2)
let H1, H2 be Subgroup of G; ::_thesis: (A * H1) * H2 = A * (H1 * H2)
thus (A * H1) * H2 = A * (H1 * (carr H2)) by GROUP_2:99
.= A * (H1 * H2) ; ::_thesis: verum
end;

theorem :: GROUP_4:48
for G being Group
for A being Subset of G
for H1, H2 being Subgroup of G holds (H1 * H2) * A = H1 * (H2 * A)
proof
let G be Group; ::_thesis: for A being Subset of G
for H1, H2 being Subgroup of G holds (H1 * H2) * A = H1 * (H2 * A)
let A be Subset of G; ::_thesis: for H1, H2 being Subgroup of G holds (H1 * H2) * A = H1 * (H2 * A)
let H1, H2 be Subgroup of G; ::_thesis: (H1 * H2) * A = H1 * (H2 * A)
thus (H1 * H2) * A = (H1 * (carr H2)) * A
.= H1 * (H2 * A) by GROUP_2:98 ; ::_thesis: verum
end;

definition
let G be Group;
let H1, H2 be Subgroup of G;
funcH1 "\/" H2 ->  strict Subgroup of G equals :: GROUP_4:def 9
 gr ((carr H1) \/ (carr H2));
correctness
coherence
gr ((carr H1) \/ (carr H2)) is strict Subgroup of G;
;
end;

:: deftheorem  defines "\/" GROUP_4:def_9_:_
 for G being Group
for H1, H2 being Subgroup of G holds H1 "\/" H2 = gr ((carr H1) \/ (carr H2));

theorem :: GROUP_4:49
for G being Group
for a being Element of G
for H1, H2 being Subgroup of G holds
( a in H1 "\/" H2 iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= (carr H1) \/ (carr H2) & a = Product (F |^ I) ) ) by Th28;

theorem :: GROUP_4:50
for G being Group
for H1, H2 being Subgroup of G holds H1 "\/" H2 = gr (H1 * H2)
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds H1 "\/" H2 = gr (H1 * H2)
let H1, H2 be Subgroup of G; ::_thesis: H1 "\/" H2 = gr (H1 * H2)
set H = gr ((carr H1) * (carr H2));
now__::_thesis:_for_a_being_Element_of_G_st_a_in_gr_((carr_H1)_*_(carr_H2))_holds_
a_in_H1_"\/"_H2
let a be Element of G; ::_thesis: ( a in gr ((carr H1) * (carr H2)) implies a in H1 "\/" H2 )
assume  a in gr ((carr H1) * (carr H2)) ; ::_thesis: a in H1 "\/" H2
then consider F being FinSequence of the carrier of G, I being FinSequence of INT  such that
A1: len F = len I and
A2: rng F c= (carr H1) * (carr H2) and
A3: a = Product (F |^ I) by Th28;
 rng (F |^ I) c= carr (H1 "\/" H2)
proof
set f = F |^ I;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (F |^ I) or x in carr (H1 "\/" H2) )
A4: rng I c= INT by FINSEQ_1:def_4;
assume  x in rng (F |^ I) ; ::_thesis: x in carr (H1 "\/" H2)
then consider y being set  such that
A5: y in dom (F |^ I) and
A6: (F |^ I) . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A5;
A7: len (F |^ I) = len F by Def3;
then A8: y in dom I by A1, A5, FINSEQ_3:29;
then A9: I /. y = I . y by PARTFUN1:def_6;
 I . y in rng I by A8, FUNCT_1:def_3;
then reconsider i = I . y as Integer by A4;
A10: @ (I /. y) = I /. y ;
 y in dom F by A5, A7, FINSEQ_3:29;
then  ( F /. y = F . y & F . y in rng F ) by FUNCT_1:def_3, PARTFUN1:def_6;
then consider b, c being Element of G such that
A11: F /. y = b * c and
A12: b in carr H1 and
A13: c in carr H2 by A2, GROUP_2:8;
 y in dom F by A5, A7, FINSEQ_3:29;
then A14: x = (F /. y) |^ i by A6, A9, A10, Def3;
now__::_thesis:_x_in_carr_(H1_"\/"_H2)
percases ( i >= 0 or i < 0 ) ;
suppose i >= 0 ; ::_thesis: x in carr (H1 "\/" H2)
then reconsider n = i as Element of NAT by INT_1:3;
defpred S1[ Nat, set ] means ( ( $1 mod 2 = 1 implies $2 = b ) & ( $1 mod 2 = 0 implies $2 = c ) );
A15: for k being Nat st k in Seg (2 * n) holds
ex x being set st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (2 * n) implies ex x being set st S1[k,x] )
assume  k in Seg (2 * n) ; ::_thesis: ex x being set st S1[k,x]
now__::_thesis:_ex_x_being_set_st_
(_(_k_mod_2_=_1_implies_x_=_b_)_&_(_k_mod_2_=_0_implies_x_=_c_)_)
percases ( k mod 2 = 1 or k mod 2 = 0 ) by NAT_D:12;
supposeA16: k mod 2 = 1 ; ::_thesis: ex x being set st
( ( k mod 2 = 1 implies x = b ) & ( k mod 2 = 0 implies x = c ) )
reconsider x = b as set ;
take x = x; ::_thesis: ( ( k mod 2 = 1 implies x = b ) & ( k mod 2 = 0 implies x = c ) )
thus  ( ( k mod 2 = 1 implies x = b ) & ( k mod 2 = 0 implies x = c ) ) by A16; ::_thesis: verum
end;
supposeA17: k mod 2 = 0 ; ::_thesis: ex x being set st
( ( k mod 2 = 1 implies x = b ) & ( k mod 2 = 0 implies x = c ) )
reconsider x = c as set ;
take x = x; ::_thesis: ( ( k mod 2 = 1 implies x = b ) & ( k mod 2 = 0 implies x = c ) )
thus  ( ( k mod 2 = 1 implies x = b ) & ( k mod 2 = 0 implies x = c ) ) by A17; ::_thesis: verum
end;
end;
end;
hence  ex x being set st S1[k,x] ; ::_thesis: verum
end;
consider p being FinSequence such that
A18: dom p = Seg (2 * n) and
A19: for k being Nat st k in Seg (2 * n) holds
S1[k,p . k] from FINSEQ_1:sch_1(A15);
A20: len p = 2 * n by A18, FINSEQ_1:def_3;
A21: rng p c= {b,c}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in {b,c} )
assume  x in rng p ; ::_thesis: x in {b,c}
then consider y being set  such that
A22: y in dom p and
A23: p . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A22;
now__::_thesis:_x_in_{b,c}
percases ( y mod 2 = 0 or y mod 2 = 1 ) by NAT_D:12;
suppose y mod 2 = 0 ; ::_thesis: x in {b,c}
then  x = c by A18, A19, A22, A23;
hence  x in {b,c} by TARSKI:def_2; ::_thesis: verum
end;
suppose y mod 2 = 1 ; ::_thesis: x in {b,c}
then  x = b by A18, A19, A22, A23;
hence  x in {b,c} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
hence  x in {b,c} ; ::_thesis: verum
end;
then  rng p c= the carrier of G by XBOOLE_1:1;
then reconsider p = p as FinSequence of the carrier of G by FINSEQ_1:def_4;
A24: ( (carr H1) \/ (carr H2) c= the carrier of (gr ((carr H1) \/ (carr H2))) & carr (gr ((carr H1) \/ (carr H2))) = the carrier of (gr ((carr H1) \/ (carr H2))) ) by Def4;
defpred S2[ Nat] means ( $1 <= 2 * n & $1 mod 2 = 0 implies for F1 being FinSequence of the carrier of G st F1 = p | (Seg $1) holds
Product F1 = (F /. y) |^ ($1 div 2) );
A25: for k being Nat st ( for l being Nat st l < k holds
S2[l] ) holds
S2[k]
proof
let k be Nat; ::_thesis: ( ( for l being Nat st l < k holds
S2[l] ) implies S2[k] )
assume A26: for l being Nat st l < k holds
S2[l] ; ::_thesis: S2[k]
assume that
A27: k <= 2 * n and
A28: k mod 2 = 0 ; ::_thesis: for F1 being FinSequence of the carrier of G st F1 = p | (Seg k) holds
Product F1 = (F /. y) |^ (k div 2)
let F1 be FinSequence of the carrier of G; ::_thesis: ( F1 = p | (Seg k) implies Product F1 = (F /. y) |^ (k div 2) )
assume A29: F1 = p | (Seg k) ; ::_thesis: Product F1 = (F /. y) |^ (k div 2)
now__::_thesis:_Product_F1_=_(F_/._y)_|^_(k_div_2)
percases ( k = 0 or k <> 0 ) ;
supposeA30: k = 0 ; ::_thesis: Product F1 = (F /. y) |^ (k div 2)
 2 * 0 = 0 ;
then A31: 0 div 2 = 0 by NAT_D:18;
 F1 = <*> the carrier of G by A29, A30;
then  Product F1 = 1_ G by Th8;
hence  Product F1 = (F /. y) |^ (k div 2) by A30, A31, GROUP_1:25; ::_thesis: verum
end;
supposeA32: k <> 0 ; ::_thesis: Product F1 = (F /. y) |^ (k div 2)
A33: k <> 1 by A28, NAT_D:14;
 k >= 1 by A32, NAT_1:14;
then  k > 1 by A33, XXREAL_0:1;
then  k >= 1 + 1 by NAT_1:13;
then  k - 2 >= 2 - 2 by XREAL_1:9;
then reconsider m = k - 2 as Element of NAT by INT_1:3;
reconsider q = p | (Seg m) as FinSequence of the carrier of G by FINSEQ_1:18;
 1 * 2 = 2 ;
then A34: m mod 2 = 0 by A28, NAT_D:15;
A35: m + 2 = k ;
then A36: m <= 2 * n by A27, NAT_1:16, XXREAL_0:2;
then  ex o being Nat st 2 * n = m + o by NAT_1:10;
then A37: len q = m by A20, FINSEQ_3:53;
A38: ex j being Nat st 2 * n = k + j by A27, NAT_1:10;
then A39: len F1 = k by A20, A29, FINSEQ_3:53;
A40: now__::_thesis:_for_l_being_Element_of_NAT_st_l_in_dom_q_holds_
F1_._l_=_q_._l
let l be Element of NAT ; ::_thesis: ( l in dom q implies F1 . l = q . l )
assume A41: l in dom q ; ::_thesis: F1 . l = q . l
then  l <= len q by FINSEQ_3:25;
then A42: l <= len F1 by A35, A39, A37, NAT_1:16, XXREAL_0:2;
 1 <= l by A41, FINSEQ_3:25;
then  l in dom F1 by A42, FINSEQ_3:25;
then  F1 . l = p . l by A29, FUNCT_1:47;
hence  F1 . l = q . l by A41, FUNCT_1:47; ::_thesis: verum
end;
A43: m < k by A35, NAT_1:16;
then A44: Product q = (F /. y) |^ (m div 2) by A26, A36, A34;
A45: now__::_thesis:_for_l_being_Element_of_NAT_st_l_in_dom_<*b,c*>_holds_
F1_._((len_q)_+_l)_=_<*b,c*>_._l
let l be Element of NAT ; ::_thesis: ( l in dom <*b,c*> implies F1 . ((len q) + l) = <*b,c*> . l )
assume  l in dom <*b,c*> ; ::_thesis: F1 . ((len q) + l) = <*b,c*> . l
then A46: l in {1,2} by FINSEQ_1:2, FINSEQ_1:89;
now__::_thesis:_F1_._((len_q)_+_l)_=_<*b,c*>_._l
percases ( l = 1 or l = 2 ) by A46, TARSKI:def_2;
supposeA47: l = 1 ; ::_thesis: F1 . ((len q) + l) = <*b,c*> . l
then A48: <*b,c*> . l = b by FINSEQ_1:44;
A49: ( (m + 1) mod 2 = 1 & dom F1 c= dom p ) by A29, A34, NAT_D:16, RELAT_1:60;
 ( m + 1 <= k & 1 <= m + 1 ) by A43, NAT_1:12, NAT_1:13;
then A50: m + 1 in dom F1 by A39, FINSEQ_3:25;
then  F1 . ((len q) + l) = p . (m + 1) by A29, A37, A47, FUNCT_1:47;
hence  F1 . ((len q) + l) = <*b,c*> . l by A18, A19, A48, A50, A49; ::_thesis: verum
end;
supposeA51: l = 2 ; ::_thesis: F1 . ((len q) + l) = <*b,c*> . l
then A52: <*b,c*> . l = c by FINSEQ_1:44;
A53: dom F1 c= dom p by A29, RELAT_1:60;
 1 <= m + (1 + 1) by NAT_1:12;
then A54: m + 2 in dom F1 by A39, FINSEQ_3:25;
then  F1 . ((len q) + l) = p . (m + 2) by A29, A37, A51, FUNCT_1:47;
hence  F1 . ((len q) + l) = <*b,c*> . l by A18, A19, A28, A52, A54, A53; ::_thesis: verum
end;
end;
end;
hence  F1 . ((len q) + l) = <*b,c*> . l ; ::_thesis: verum
end;
A55: (m div (2 * 1)) + 1 = (m div 2) + (2 div 2) by NAT_D:18
.= k div 2 by A35, A34, NAT_D:19 ;
len F1 = m + 2 by A20, A29, A38, FINSEQ_3:53
.= (len q) + (len <*b,c*>) by A37, FINSEQ_1:44 ;
then  F1 = q ^ <*b,c*> by A40, A45, FINSEQ_3:38;
then  Product F1 = (Product q) * (Product <*b,c*>) by FINSOP_1:5
.= (Product q) * (F /. y) by A11, FINSOP_1:12
.= (F /. y) |^ ((m div 2) + 1) by A44, GROUP_1:34 ;
hence  Product F1 = (F /. y) |^ (k div 2) by A55; ::_thesis: verum
end;
end;
end;
hence  Product F1 = (F /. y) |^ (k div 2) ; ::_thesis: verum
end;
A56: for k being Nat holds S2[k] from NAT_1:sch_4(A25);
 ( b in (carr H1) \/ (carr H2) & c in (carr H1) \/ (carr H2) ) by A12, A13, XBOOLE_0:def_3;
then  {b,c} c= (carr H1) \/ (carr H2) by ZFMISC_1:32;
then A57: rng p c= (carr H1) \/ (carr H2) by A21, XBOOLE_1:1;
 len p = 2 * n by A18, FINSEQ_1:def_3;
then A58: p = p | (Seg (2 * n)) by FINSEQ_3:49;
 ( (2 * n) mod 2 = 0 & (2 * n) div 2 = n ) by NAT_D:13, NAT_D:18;
then  x = Product p by A14, A56, A58;
then  x in gr ((carr H1) \/ (carr H2)) by A57, A24, Th18, XBOOLE_1:1;
hence  x in carr (H1 "\/" H2) by STRUCT_0:def_5; ::_thesis: verum
end;
supposeA59: i < 0 ; ::_thesis: x in carr (H1 "\/" H2)
defpred S1[ Nat, set ] means ( ( $1 mod 2 = 1 implies $2 = c " ) & ( $1 mod 2 = 0 implies $2 = b " ) );
set n = abs i;
A60: ( (2 * (abs i)) mod 2 = 0 & (2 * (abs i)) div 2 = abs i ) by NAT_D:13, NAT_D:18;
A61: for k being Nat st k in Seg (2 * (abs i)) holds
ex x being set st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (2 * (abs i)) implies ex x being set st S1[k,x] )
assume  k in Seg (2 * (abs i)) ; ::_thesis: ex x being set st S1[k,x]
now__::_thesis:_ex_x_being_set_st_
(_(_k_mod_2_=_1_implies_x_=_c_"_)_&_(_k_mod_2_=_0_implies_x_=_b_"_)_)
percases ( k mod 2 = 1 or k mod 2 = 0 ) by NAT_D:12;
supposeA62: k mod 2 = 1 ; ::_thesis: ex x being set st
( ( k mod 2 = 1 implies x = c " ) & ( k mod 2 = 0 implies x = b " ) )
reconsider x = c " as set ;
take x = x; ::_thesis: ( ( k mod 2 = 1 implies x = c " ) & ( k mod 2 = 0 implies x = b " ) )
thus  ( ( k mod 2 = 1 implies x = c " ) & ( k mod 2 = 0 implies x = b " ) ) by A62; ::_thesis: verum
end;
supposeA63: k mod 2 = 0 ; ::_thesis: ex x being set st
( ( k mod 2 = 1 implies x = c " ) & ( k mod 2 = 0 implies x = b " ) )
reconsider x = b " as set ;
take x = x; ::_thesis: ( ( k mod 2 = 1 implies x = c " ) & ( k mod 2 = 0 implies x = b " ) )
thus  ( ( k mod 2 = 1 implies x = c " ) & ( k mod 2 = 0 implies x = b " ) ) by A63; ::_thesis: verum
end;
end;
end;
hence  ex x being set st S1[k,x] ; ::_thesis: verum
end;
consider p being FinSequence such that
A64: dom p = Seg (2 * (abs i)) and
A65: for k being Nat st k in Seg (2 * (abs i)) holds
S1[k,p . k] from FINSEQ_1:sch_1(A61);
A66: len p = 2 * (abs i) by A64, FINSEQ_1:def_3;
A67: rng p c= {(b "),(c ")}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in {(b "),(c ")} )
assume  x in rng p ; ::_thesis: x in {(b "),(c ")}
then consider y being set  such that
A68: y in dom p and
A69: p . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A68;
now__::_thesis:_x_in_{(b_"),(c_")}
percases ( y mod 2 = 0 or y mod 2 = 1 ) by NAT_D:12;
suppose y mod 2 = 0 ; ::_thesis: x in {(b "),(c ")}
then  x = b " by A64, A65, A68, A69;
hence  x in {(b "),(c ")} by TARSKI:def_2; ::_thesis: verum
end;
suppose y mod 2 = 1 ; ::_thesis: x in {(b "),(c ")}
then  x = c " by A64, A65, A68, A69;
hence  x in {(b "),(c ")} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
hence  x in {(b "),(c ")} ; ::_thesis: verum
end;
then  rng p c= the carrier of G by XBOOLE_1:1;
then reconsider p = p as FinSequence of the carrier of G by FINSEQ_1:def_4;
A70: ( (carr H1) \/ (carr H2) c= the carrier of (gr ((carr H1) \/ (carr H2))) & carr (gr ((carr H1) \/ (carr H2))) = the carrier of (gr ((carr H1) \/ (carr H2))) ) by Def4;
defpred S2[ Nat] means ( $1 <= 2 * (abs i) & $1 mod 2 = 0 implies for F1 being FinSequence of the carrier of G st F1 = p | (Seg $1) holds
Product F1 = ((F /. y) |^ ($1 div 2)) " );
A71: for k being Nat st ( for l being Nat st l < k holds
S2[l] ) holds
S2[k]
proof
let k be Nat; ::_thesis: ( ( for l being Nat st l < k holds
S2[l] ) implies S2[k] )
assume A72: for l being Nat st l < k holds
S2[l] ; ::_thesis: S2[k]
assume that
A73: k <= 2 * (abs i) and
A74: k mod 2 = 0 ; ::_thesis: for F1 being FinSequence of the carrier of G st F1 = p | (Seg k) holds
Product F1 = ((F /. y) |^ (k div 2)) "
let F1 be FinSequence of the carrier of G; ::_thesis: ( F1 = p | (Seg k) implies Product F1 = ((F /. y) |^ (k div 2)) " )
assume A75: F1 = p | (Seg k) ; ::_thesis: Product F1 = ((F /. y) |^ (k div 2)) "
now__::_thesis:_Product_F1_=_((F_/._y)_|^_(k_div_2))_"
percases ( k = 0 or k <> 0 ) ;
supposeA76: k = 0 ; ::_thesis: Product F1 = ((F /. y) |^ (k div 2)) "
 2 * 0 = 0 ;
then  0 div 2 = 0 by NAT_D:18;
then A77: (F /. y) |^ (k div 2) = 1_ G by A76, GROUP_1:25;
 F1 = <*> the carrier of G by A75, A76;
then  Product F1 = 1_ G by Th8;
hence  Product F1 = ((F /. y) |^ (k div 2)) " by A77, GROUP_1:8; ::_thesis: verum
end;
supposeA78: k <> 0 ; ::_thesis: Product F1 = ((F /. y) |^ (k div 2)) "
A79: k <> 1 by A74, NAT_D:14;
 k >= 1 by A78, NAT_1:14;
then  k > 1 by A79, XXREAL_0:1;
then  k >= 1 + 1 by NAT_1:13;
then  k - 2 >= 2 - 2 by XREAL_1:9;
then reconsider m = k - 2 as Element of NAT by INT_1:3;
reconsider q = p | (Seg m) as FinSequence of the carrier of G by FINSEQ_1:18;
 1 * 2 = 2 ;
then A80: m mod 2 = 0 by A74, NAT_D:15;
A81: m + 2 = k ;
then A82: m <= 2 * (abs i) by A73, NAT_1:16, XXREAL_0:2;
then  ex o being Nat st 2 * (abs i) = m + o by NAT_1:10;
then A83: len q = m by A66, FINSEQ_3:53;
A84: ex j being Nat st 2 * (abs i) = k + j by A73, NAT_1:10;
then A85: len F1 = k by A66, A75, FINSEQ_3:53;
A86: now__::_thesis:_for_l_being_Element_of_NAT_st_l_in_dom_q_holds_
F1_._l_=_q_._l
let l be Element of NAT ; ::_thesis: ( l in dom q implies F1 . l = q . l )
assume A87: l in dom q ; ::_thesis: F1 . l = q . l
then  l <= len q by FINSEQ_3:25;
then A88: l <= len F1 by A81, A85, A83, NAT_1:16, XXREAL_0:2;
 1 <= l by A87, FINSEQ_3:25;
then  l in dom F1 by A88, FINSEQ_3:25;
then  F1 . l = p . l by A75, FUNCT_1:47;
hence  F1 . l = q . l by A87, FUNCT_1:47; ::_thesis: verum
end;
A89: m < k by A81, NAT_1:16;
then A90: Product q = ((F /. y) |^ (m div 2)) " by A72, A82, A80;
A91: now__::_thesis:_for_l_being_Element_of_NAT_st_l_in_dom_<*(c_"),(b_")*>_holds_
F1_._((len_q)_+_l)_=_<*(c_"),(b_")*>_._l
let l be Element of NAT ; ::_thesis: ( l in dom <*(c "),(b ")*> implies F1 . ((len q) + l) = <*(c "),(b ")*> . l )
assume  l in dom <*(c "),(b ")*> ; ::_thesis: F1 . ((len q) + l) = <*(c "),(b ")*> . l
then A92: l in {1,2} by FINSEQ_1:2, FINSEQ_1:89;
now__::_thesis:_F1_._((len_q)_+_l)_=_<*(c_"),(b_")*>_._l
percases ( l = 1 or l = 2 ) by A92, TARSKI:def_2;
supposeA93: l = 1 ; ::_thesis: F1 . ((len q) + l) = <*(c "),(b ")*> . l
then A94: <*(c "),(b ")*> . l = c " by FINSEQ_1:44;
A95: ( (m + 1) mod 2 = 1 & dom F1 c= dom p ) by A75, A80, NAT_D:16, RELAT_1:60;
 ( m + 1 <= k & 1 <= m + 1 ) by A89, NAT_1:12, NAT_1:13;
then A96: m + 1 in dom F1 by A85, FINSEQ_3:25;
then  F1 . ((len q) + l) = p . (m + 1) by A75, A83, A93, FUNCT_1:47;
hence  F1 . ((len q) + l) = <*(c "),(b ")*> . l by A64, A65, A94, A96, A95; ::_thesis: verum
end;
supposeA97: l = 2 ; ::_thesis: F1 . ((len q) + l) = <*(c "),(b ")*> . l
then A98: <*(c "),(b ")*> . l = b " by FINSEQ_1:44;
A99: dom F1 c= dom p by A75, RELAT_1:60;
 1 <= m + (1 + 1) by NAT_1:12;
then A100: m + 2 in dom F1 by A85, FINSEQ_3:25;
then  F1 . ((len q) + l) = p . (m + 2) by A75, A83, A97, FUNCT_1:47;
hence  F1 . ((len q) + l) = <*(c "),(b ")*> . l by A64, A65, A74, A98, A100, A99; ::_thesis: verum
end;
end;
end;
hence  F1 . ((len q) + l) = <*(c "),(b ")*> . l ; ::_thesis: verum
end;
A101: (m div (2 * 1)) + 1 = (m div 2) + (2 div 2) by NAT_D:18
.= k div 2 by A81, A80, NAT_D:19 ;
len F1 = m + 2 by A66, A75, A84, FINSEQ_3:53
.= (len q) + (len <*(c "),(b ")*>) by A83, FINSEQ_1:44 ;
then  F1 = q ^ <*(c "),(b ")*> by A86, A91, FINSEQ_3:38;
then  Product F1 = (Product q) * (Product <*(c "),(b ")*>) by FINSOP_1:5
.= (Product q) * ((c ") * (b ")) by FINSOP_1:12
.= (Product q) * ((F /. y) ") by A11, GROUP_1:17
.= ((F /. y) * ((F /. y) |^ (m div 2))) " by A90, GROUP_1:17
.= ((F /. y) |^ ((m div 2) + 1)) " by GROUP_1:34 ;
hence  Product F1 = ((F /. y) |^ (k div 2)) " by A101; ::_thesis: verum
end;
end;
end;
hence  Product F1 = ((F /. y) |^ (k div 2)) " ; ::_thesis: verum
end;
A102: for k being Nat holds S2[k] from NAT_1:sch_4(A71);
 c " in carr H2 by A13, GROUP_2:75;
then A103: c " in (carr H1) \/ (carr H2) by XBOOLE_0:def_3;
 len p = 2 * (abs i) by A64, FINSEQ_1:def_3;
then A104: p = p | (Seg (2 * (abs i))) by FINSEQ_3:49;
 b " in carr H1 by A12, GROUP_2:75;
then  b " in (carr H1) \/ (carr H2) by XBOOLE_0:def_3;
then  {(b "),(c ")} c= (carr H1) \/ (carr H2) by A103, ZFMISC_1:32;
then A105: rng p c= (carr H1) \/ (carr H2) by A67, XBOOLE_1:1;
 x = ((F /. y) |^ (abs i)) " by A14, A59, GROUP_1:30;
then  x = Product p by A102, A60, A104;
then  x in gr ((carr H1) \/ (carr H2)) by A105, A70, Th18, XBOOLE_1:1;
hence  x in carr (H1 "\/" H2) by STRUCT_0:def_5; ::_thesis: verum
end;
end;
end;
hence  x in carr (H1 "\/" H2) ; ::_thesis: verum
end;
hence  a in H1 "\/" H2 by A3, Th18; ::_thesis: verum
end;
then A106: gr ((carr H1) * (carr H2)) is Subgroup of H1 "\/" H2 by GROUP_2:58;
 (carr H1) \/ (carr H2) 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 H1) * (carr H2) )
assume A107: x in (carr H1) \/ (carr H2) ; ::_thesis: x in (carr H1) * (carr H2)
then reconsider a = x as Element of G ;
now__::_thesis:_x_in_(carr_H1)_*_(carr_H2)
percases ( x in carr H1 or x in carr H2 ) by A107, XBOOLE_0:def_3;
supposeA108: x in carr H1 ; ::_thesis: x in (carr H1) * (carr H2)
 1_ G in H2 by GROUP_2:46;
then A109: 1_ G in carr H2 by STRUCT_0:def_5;
 a * (1_ G) = a by GROUP_1:def_4;
hence  x in (carr H1) * (carr H2) by A108, A109; ::_thesis: verum
end;
supposeA110: x in carr H2 ; ::_thesis: x in (carr H1) * (carr H2)
 1_ G in H1 by GROUP_2:46;
then A111: 1_ G in carr H1 by STRUCT_0:def_5;
 (1_ G) * a = a by GROUP_1:def_4;
hence  x in (carr H1) * (carr H2) by A110, A111; ::_thesis: verum
end;
end;
end;
hence  x in (carr H1) * (carr H2) ; ::_thesis: verum
end;
then  H1 "\/" H2 is Subgroup of gr ((carr H1) * (carr H2)) by Th32;
hence  gr (H1 * H2) = H1 "\/" H2 by A106, GROUP_2:55; ::_thesis: verum
end;

theorem Th51: :: GROUP_4:51
for G being Group
for H1, H2 being Subgroup of G st H1 * H2 = H2 * H1 holds
the carrier of (H1 "\/" H2) = H1 * H2
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G st H1 * H2 = H2 * H1 holds
the carrier of (H1 "\/" H2) = H1 * H2
let H1, H2 be Subgroup of G; ::_thesis: ( H1 * H2 = H2 * H1 implies the carrier of (H1 "\/" H2) = H1 * H2 )
assume  H1 * H2 = H2 * H1 ; ::_thesis: the carrier of (H1 "\/" H2) = H1 * H2
then consider H being strict Subgroup of G such that
A1: the carrier of H = (carr H1) * (carr H2) by GROUP_2:78;
now__::_thesis:_for_a_being_Element_of_G_st_a_in_H_holds_
a_in_H1_"\/"_H2
reconsider p = 1 as Integer ;
let a be Element of G; ::_thesis: ( a in H implies a in H1 "\/" H2 )
assume  a in H ; ::_thesis: a in H1 "\/" H2
then  a in (carr H1) * (carr H2) by A1, STRUCT_0:def_5;
then consider b, c being Element of G such that
A2: a = b * c and
A3: ( b in carr H1 & c in carr H2 ) ;
 ( b in (carr H1) \/ (carr H2) & c in (carr H1) \/ (carr H2) ) by A3, XBOOLE_0:def_3;
then A4: ( rng <*b,c*> = {b,c} & {b,c} c= (carr H1) \/ (carr H2) ) by FINSEQ_2:127, ZFMISC_1:32;
A5: ( len <*b,c*> = 2 & len <*(@ p),(@ p)*> = 2 ) by FINSEQ_1:44;
a = (Product <*b*>) * c by A2, FINSOP_1:11
.= (Product <*b*>) * (Product <*c*>) by FINSOP_1:11
.= Product (<*b*> ^ <*c*>) by FINSOP_1:5
.= Product <*b,c*> by FINSEQ_1:def_9
.= Product <*(b |^ p),c*> by GROUP_1:26
.= Product <*(b |^ p),(c |^ p)*> by GROUP_1:26
.= Product (<*b,c*> |^ <*(@ p),(@ p)*>) by Th23 ;
hence  a in H1 "\/" H2 by A5, A4, Th28; ::_thesis: verum
end;
then A6: H is Subgroup of H1 "\/" H2 by GROUP_2:58;
 (carr H1) \/ (carr H2) 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 H1) * (carr H2) )
assume A7: x in (carr H1) \/ (carr H2) ; ::_thesis: x in (carr H1) * (carr H2)
then reconsider a = x as Element of G ;
now__::_thesis:_x_in_(carr_H1)_*_(carr_H2)
percases ( x in carr H1 or x in carr H2 ) by A7, XBOOLE_0:def_3;
supposeA8: x in carr H1 ; ::_thesis: x in (carr H1) * (carr H2)
 1_ G in H2 by GROUP_2:46;
then A9: 1_ G in carr H2 by STRUCT_0:def_5;
 a * (1_ G) = a by GROUP_1:def_4;
hence  x in (carr H1) * (carr H2) by A8, A9; ::_thesis: verum
end;
supposeA10: x in carr H2 ; ::_thesis: x in (carr H1) * (carr H2)
 1_ G in H1 by GROUP_2:46;
then A11: 1_ G in carr H1 by STRUCT_0:def_5;
 (1_ G) * a = a by GROUP_1:def_4;
hence  x in (carr H1) * (carr H2) by A10, A11; ::_thesis: verum
end;
end;
end;
hence  x in (carr H1) * (carr H2) ; ::_thesis: verum
end;
then  H1 "\/" H2 is Subgroup of H by A1, Def4;
hence  the carrier of (H1 "\/" H2) = H1 * H2 by A1, A6, GROUP_2:55; ::_thesis: verum
end;

theorem :: GROUP_4:52
for G being Group
for H1, H2 being Subgroup of G st G is commutative Group holds
the carrier of (H1 "\/" H2) = H1 * H2
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G st G is commutative Group holds
the carrier of (H1 "\/" H2) = H1 * H2
let H1, H2 be Subgroup of G; ::_thesis: ( G is commutative Group implies the carrier of (H1 "\/" H2) = H1 * H2 )
assume  G is commutative Group ; ::_thesis: the carrier of (H1 "\/" H2) = H1 * H2
then  H1 * H2 = H2 * H1 by GROUP_2:25;
hence  the carrier of (H1 "\/" H2) = H1 * H2 by Th51; ::_thesis: verum
end;

theorem Th53: :: GROUP_4:53
for G being Group
for N1, N2 being strict normal Subgroup of G holds the carrier of (N1 "\/" N2) = N1 * N2
proof
let G be Group; ::_thesis: for N1, N2 being strict normal Subgroup of G holds the carrier of (N1 "\/" N2) = N1 * N2
let N1, N2 be strict normal Subgroup of G; ::_thesis: the carrier of (N1 "\/" N2) = N1 * N2
 N1 * N2 = N2 * N1 by GROUP_3:125;
hence  the carrier of (N1 "\/" N2) = N1 * N2 by Th51; ::_thesis: verum
end;

theorem :: GROUP_4:54
for G being Group
for N1, N2 being strict normal Subgroup of G holds N1 "\/" N2 is normal Subgroup of G
proof
let G be Group; ::_thesis: for N1, N2 being strict normal Subgroup of G holds N1 "\/" N2 is normal Subgroup of G
let N1, N2 be strict normal Subgroup of G; ::_thesis: N1 "\/" N2 is normal Subgroup of G
 ( ex N being strict normal Subgroup of G st the carrier of N = (carr N1) * (carr N2) & the carrier of (N1 "\/" N2) = N1 * N2 ) by Th53, GROUP_3:126;
hence  N1 "\/" N2 is normal Subgroup of G by GROUP_2:59; ::_thesis: verum
end;

theorem :: GROUP_4:55
for G being Group
for H being strict Subgroup of G holds H "\/" H = H by Th31;

theorem :: GROUP_4:56
for G being Group
for H1, H2 being Subgroup of G holds H1 "\/" H2 = H2 "\/" H1 ;

Lm4:  for G being Group
for H1, H2 being Subgroup of G holds H1 is Subgroup of H1 "\/" H2
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds H1 is Subgroup of H1 "\/" H2
let H1, H2 be Subgroup of G; ::_thesis: H1 is Subgroup of H1 "\/" H2
 ( carr H1 c= (carr H1) \/ (carr H2) & (carr H1) \/ (carr H2) c= the carrier of (gr ((carr H1) \/ (carr H2))) ) by Def4, XBOOLE_1:7;
hence  H1 is Subgroup of H1 "\/" H2 by GROUP_2:57, XBOOLE_1:1; ::_thesis: verum
end;

Lm5:  for G being Group
for H1, H2, H3 being Subgroup of G holds (H1 "\/" H2) "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3)
proof
let G be Group; ::_thesis: for H1, H2, H3 being Subgroup of G holds (H1 "\/" H2) "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3)
let H1, H2, H3 be Subgroup of G; ::_thesis: (H1 "\/" H2) "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3)
now__::_thesis:_for_a_being_Element_of_G_st_a_in_(H1_"\/"_H2)_"\/"_H3_holds_
a_in_H1_"\/"_(H2_"\/"_H3)
let a be Element of G; ::_thesis: ( a in (H1 "\/" H2) "\/" H3 implies a in H1 "\/" (H2 "\/" H3) )
assume  a in (H1 "\/" H2) "\/" H3 ; ::_thesis: a in H1 "\/" (H2 "\/" H3)
then consider F being FinSequence of the carrier of G, I being FinSequence of INT  such that
A1: len F = len I and
A2: rng F c= (carr (H1 "\/" H2)) \/ (carr H3) and
A3: a = Product (F |^ I) by Th28;
 rng F c= carr (gr ((carr H1) \/ (carr (H2 "\/" H3))))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3)))) )
assume A4: x in rng F ; ::_thesis: x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3))))
now__::_thesis:_x_in_carr_(gr_((carr_H1)_\/_(carr_(H2_"\/"_H3))))
percases ( x in carr (H1 "\/" H2) or x in carr H3 ) by A2, A4, XBOOLE_0:def_3;
supposeA5: x in carr (H1 "\/" H2) ; ::_thesis: x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3))))
then reconsider b = x as Element of G ;
 x in H1 "\/" H2 by A5, STRUCT_0:def_5;
then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT  such that
A6: len F1 = len I1 and
A7: rng F1 c= (carr H1) \/ (carr H2) and
A8: b = Product (F1 |^ I1) by Th28;
 H2 is Subgroup of H2 "\/" H3 by Lm4;
then  the carrier of H2 c= the carrier of (H2 "\/" H3) by GROUP_2:def_5;
then  (carr H1) \/ (carr H2) c= (carr H1) \/ (carr (H2 "\/" H3)) by XBOOLE_1:9;
then  rng F1 c= (carr H1) \/ (carr (H2 "\/" H3)) by A7, XBOOLE_1:1;
then  b in H1 "\/" (H2 "\/" H3) by A6, A8, Th28;
hence  x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3)))) by STRUCT_0:def_5; ::_thesis: verum
end;
supposeA9: x in carr H3 ; ::_thesis: x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3))))
A10: H3 is Subgroup of H3 "\/" H2 by Lm4;
 x in H3 by A9, STRUCT_0:def_5;
then  x in H3 "\/" H2 by A10, GROUP_2:40;
then  x in carr (H2 "\/" H3) by STRUCT_0:def_5;
then A11: x in (carr H1) \/ (carr (H2 "\/" H3)) by XBOOLE_0:def_3;
 (carr H1) \/ (carr (H2 "\/" H3)) c= the carrier of (gr ((carr H1) \/ (carr (H2 "\/" H3)))) by Def4;
hence  x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3)))) by A11; ::_thesis: verum
end;
end;
end;
hence  x in carr (gr ((carr H1) \/ (carr (H2 "\/" H3)))) ; ::_thesis: verum
end;
then  a in gr (carr (gr ((carr H1) \/ (carr (H2 "\/" H3))))) by A1, A3, Th28;
hence  a in H1 "\/" (H2 "\/" H3) by Th31; ::_thesis: verum
end;
hence  (H1 "\/" H2) "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3) by GROUP_2:58; ::_thesis: verum
end;

theorem Th57: :: GROUP_4:57
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)
 ( (H2 "\/" H3) "\/" H1 is Subgroup of H2 "\/" (H3 "\/" H1) & (H3 "\/" H1) "\/" H2 is Subgroup of H3 "\/" (H1 "\/" H2) ) by Lm5;
then A1: H1 "\/" (H2 "\/" H3) is Subgroup of H3 "\/" (H1 "\/" H2) by GROUP_2:56;
 (H1 "\/" H2) "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3) by Lm5;
hence  (H1 "\/" H2) "\/" H3 = H1 "\/" (H2 "\/" H3) by A1, GROUP_2:55; ::_thesis: verum
end;

theorem :: GROUP_4:58
for G being Group
for H being strict Subgroup of G holds
( ((1). G) "\/" H = H & H "\/" ((1). G) = H )
proof
let G be Group; ::_thesis: for H being strict Subgroup of G holds
( ((1). G) "\/" H = H & H "\/" ((1). G) = H )
let H be strict Subgroup of G; ::_thesis: ( ((1). G) "\/" H = H & H "\/" ((1). G) = H )
 1_ G in H by GROUP_2:46;
then  1_ G in carr H by STRUCT_0:def_5;
then  {(1_ G)} c= carr H by ZFMISC_1:31;
then A1: ( carr ((1). G) = {(1_ G)} & {(1_ G)} \/ (carr H) = carr H ) by GROUP_2:def_7, XBOOLE_1:12;
hence  ((1). G) "\/" H = H by Th31; ::_thesis: H "\/" ((1). G) = H
thus  H "\/" ((1). G) = H by A1, Th31; ::_thesis: verum
end;

theorem Th59: :: GROUP_4:59
for G being Group
for H being Subgroup of G holds
( ((Omega). G) "\/" H = (Omega). G & H "\/" ((Omega). G) = (Omega). G )
proof
let G be Group; ::_thesis: for H being Subgroup of G holds
( ((Omega). G) "\/" H = (Omega). G & H "\/" ((Omega). G) = (Omega). G )
let H be Subgroup of G; ::_thesis: ( ((Omega). G) "\/" H = (Omega). G & H "\/" ((Omega). G) = (Omega). G )
A1: the carrier of ((Omega). G) \/ (carr H) = [#] the carrier of G by SUBSET_1:11;
hence  ((Omega). G) "\/" H = (Omega). G by Th31; ::_thesis: H "\/" ((Omega). G) = (Omega). G
thus  H "\/" ((Omega). G) = (Omega). G by A1, Th31; ::_thesis: verum
end;

theorem Th60: :: GROUP_4:60
for G being Group
for H1, H2 being Subgroup of G holds
( H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2 )
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds
( H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2 )
let H1, H2 be Subgroup of G; ::_thesis: ( H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2 )
 H1 "\/" H2 = H2 "\/" H1 ;
hence  ( H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2 ) by Lm4; ::_thesis: verum
end;

theorem Th61: :: GROUP_4:61
for G being Group
for H1 being Subgroup of G
for H2 being strict Subgroup of G holds
( H1 is Subgroup of H2 iff H1 "\/" H2 = H2 )
proof
let G be Group; ::_thesis: for H1 being Subgroup of G
for H2 being strict Subgroup of G holds
( H1 is Subgroup of H2 iff H1 "\/" H2 = H2 )
let H1 be Subgroup of G; ::_thesis: for H2 being strict Subgroup of G holds
( H1 is Subgroup of H2 iff H1 "\/" H2 = H2 )
let H2 be strict Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 iff H1 "\/" H2 = H2 )
thus  ( H1 is Subgroup of H2 implies H1 "\/" H2 = H2 ) ::_thesis: ( H1 "\/" H2 = H2 implies H1 is Subgroup of H2 )
proof
assume  H1 is Subgroup of H2 ; ::_thesis: H1 "\/" H2 = H2
then  the carrier of H1 c= the carrier of H2 by GROUP_2:def_5;
hence H1 "\/" H2 = gr (carr H2) by XBOOLE_1:12
.= H2 by Th31 ;
::_thesis: verum
end;
thus  ( H1 "\/" H2 = H2 implies H1 is Subgroup of H2 ) by Th60; ::_thesis: verum
end;

theorem :: GROUP_4:62
for G being Group
for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 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 holds
H1 is Subgroup of H2 "\/" H3
let H1, H2, H3 be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 implies H1 is Subgroup of H2 "\/" H3 )
 H2 is Subgroup of H2 "\/" H3 by Th60;
hence  ( H1 is Subgroup of H2 implies H1 is Subgroup of H2 "\/" H3 ) by GROUP_2:56; ::_thesis: verum
end;

theorem :: GROUP_4:63
for G being Group
for H1, H2 being Subgroup of G
for H3 being strict Subgroup of G st H1 is Subgroup of H3 & H2 is Subgroup of H3 holds
H1 "\/" H2 is Subgroup of H3
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G
for H3 being strict Subgroup of G st H1 is Subgroup of H3 & H2 is Subgroup of H3 holds
H1 "\/" H2 is Subgroup of H3
let H1, H2 be Subgroup of G; ::_thesis: for H3 being strict Subgroup of G st H1 is Subgroup of H3 & H2 is Subgroup of H3 holds
H1 "\/" H2 is Subgroup of H3
let H3 be strict Subgroup of G; ::_thesis: ( H1 is Subgroup of H3 & H2 is Subgroup of H3 implies H1 "\/" H2 is Subgroup of H3 )
assume A1: ( H1 is Subgroup of H3 & H2 is Subgroup of H3 ) ; ::_thesis: H1 "\/" H2 is Subgroup of H3
now__::_thesis:_for_a_being_Element_of_G_st_a_in_H1_"\/"_H2_holds_
a_in_H3
let a be Element of G; ::_thesis: ( a in H1 "\/" H2 implies a in H3 )
assume  a in H1 "\/" H2 ; ::_thesis: a in H3
then consider F being FinSequence of the carrier of G, I being FinSequence of INT  such that
A2: len F = len I and
A3: rng F c= (carr H1) \/ (carr H2) and
A4: a = Product (F |^ I) by Th28;
 ( the carrier of H1 c= the carrier of H3 & the carrier of H2 c= the carrier of H3 ) by A1, GROUP_2:def_5;
then  (carr H1) \/ (carr H2) c= carr H3 by XBOOLE_1:8;
then  rng F c= carr H3 by A3, XBOOLE_1:1;
then  a in gr (carr H3) by A2, A4, Th28;
hence  a in H3 by Th31; ::_thesis: verum
end;
hence  H1 "\/" H2 is Subgroup of H3 by GROUP_2:58; ::_thesis: verum
end;

theorem :: GROUP_4:64
for G being Group
for H1 being Subgroup of G
for H3, H2 being strict 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 being Subgroup of G
for H3, H2 being strict Subgroup of G st H1 is Subgroup of H2 holds
H1 "\/" H3 is Subgroup of H2 "\/" H3
let H1 be Subgroup of G; ::_thesis: for H3, H2 being strict Subgroup of G st H1 is Subgroup of H2 holds
H1 "\/" H3 is Subgroup of H2 "\/" H3
let H3, H2 be strict Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 implies H1 "\/" H3 is Subgroup of H2 "\/" H3 )
assume A1: H1 is Subgroup of H2 ; ::_thesis: H1 "\/" H3 is Subgroup of H2 "\/" H3
(H1 "\/" H3) "\/" (H2 "\/" H3) = ((H1 "\/" H3) "\/" H2) "\/" H3 by Th57
.= (H1 "\/" (H3 "\/" H2)) "\/" H3 by Th57
.= (H1 "\/" (H2 "\/" H3)) "\/" H3
.= ((H1 "\/" H2) "\/" H3) "\/" H3 by Th57
.= (H2 "\/" H3) "\/" H3 by A1, Th61
.= H2 "\/" (H3 "\/" H3) by Th57
.= H2 "\/" H3 by Th31 ;
hence  H1 "\/" H3 is Subgroup of H2 "\/" H3 by Th61; ::_thesis: verum
end;

theorem :: GROUP_4:65
for G being Group
for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1 "\/" H2
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1 "\/" H2
let H1, H2 be Subgroup of G; ::_thesis: H1 /\ H2 is Subgroup of H1 "\/" H2
 ( H1 /\ H2 is Subgroup of H1 & H1 is Subgroup of H1 "\/" H2 ) by Th60, GROUP_2:88;
hence  H1 /\ H2 is Subgroup of H1 "\/" H2 by GROUP_2:56; ::_thesis: verum
end;

theorem Th66: :: GROUP_4:66
for G being Group
for H1 being Subgroup of G
for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2
proof
let G be Group; ::_thesis: for H1 being Subgroup of G
for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2
let H1 be Subgroup of G; ::_thesis: for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2
let H2 be strict Subgroup of G; ::_thesis: (H1 /\ H2) "\/" H2 = H2
 H1 /\ H2 is Subgroup of H2 by GROUP_2:88;
hence  (H1 /\ H2) "\/" H2 = H2 by Th61; ::_thesis: verum
end;

theorem Th67: :: GROUP_4:67
for G being Group
for H2 being Subgroup of G
for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1
proof
let G be Group; ::_thesis: for H2 being Subgroup of G
for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1
let H2 be Subgroup of G; ::_thesis: for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1
let H1 be strict Subgroup of G; ::_thesis: H1 /\ (H1 "\/" H2) = H1
 H1 is Subgroup of H1 "\/" H2 by Th60;
hence  H1 /\ (H1 "\/" H2) = H1 by GROUP_2:89; ::_thesis: verum
end;

theorem :: GROUP_4:68
for G being Group
for H1, H2 being strict Subgroup of G holds
( H1 "\/" H2 = H2 iff H1 /\ H2 = H1 )
proof
let G be Group; ::_thesis: for H1, H2 being strict Subgroup of G holds
( H1 "\/" H2 = H2 iff H1 /\ H2 = H1 )
let H1, H2 be strict Subgroup of G; ::_thesis: ( H1 "\/" H2 = H2 iff H1 /\ H2 = H1 )
 ( H1 "\/" H2 = H2 iff H1 is Subgroup of H2 ) by Th61;
hence  ( H1 "\/" H2 = H2 iff H1 /\ H2 = H1 ) by GROUP_2:89; ::_thesis: verum
end;


definition
let G be Group;
func SubJoin G ->  BinOp of (Subgroups G) means :Def10: :: GROUP_4:def 10
 for H1, H2 being strict Subgroup of G holds it . (H1,H2) = H1 "\/" H2;
existence
 ex b1 being BinOp of (Subgroups G) st
for H1, H2 being strict Subgroup of G holds b1 . (H1,H2) = H1 "\/" H2
proof
defpred S1[ set , set , set ] means  for H1, H2 being Subgroup of G st $1 = H1 & $2 = H2 holds
$3 = H1 "\/" H2;
A1: for S1, S2 being Element of Subgroups G ex B being Element of Subgroups G st S1[S1,S2,B]
proof
let S1, S2 be Element of Subgroups G; ::_thesis: ex B being Element of Subgroups G st S1[S1,S2,B]
reconsider H1 = S1, H2 = S2 as Subgroup of G by GROUP_3:def_1;
reconsider C = H1 "\/" H2 as Element of Subgroups G by GROUP_3:def_1;
take  C ; ::_thesis: S1[S1,S2,C]
thus  S1[S1,S2,C] ; ::_thesis: verum
end;
consider o being BinOp of (Subgroups G) such that
A2: for a, b being Element of Subgroups G holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1);
take  o ; ::_thesis: for H1, H2 being strict Subgroup of G holds o . (H1,H2) = H1 "\/" H2
let H1, H2 be strict Subgroup of G; ::_thesis: o . (H1,H2) = H1 "\/" H2
 ( H1 in Subgroups G & H2 in Subgroups G ) by GROUP_3:def_1;
hence  o . (H1,H2) = H1 "\/" H2 by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (Subgroups G) st ( for H1, H2 being strict Subgroup of G holds b1 . (H1,H2) = H1 "\/" H2 ) & ( for H1, H2 being strict Subgroup of G holds b2 . (H1,H2) = H1 "\/" H2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (Subgroups G); ::_thesis: ( ( for H1, H2 being strict Subgroup of G holds o1 . (H1,H2) = H1 "\/" H2 ) & ( for H1, H2 being strict Subgroup of G holds o2 . (H1,H2) = H1 "\/" H2 ) implies o1 = o2 )
assume that
A3: for H1, H2 being strict Subgroup of G holds o1 . (H1,H2) = H1 "\/" H2 and
A4: for H1, H2 being strict Subgroup of G holds o2 . (H1,H2) = H1 "\/" H2 ; ::_thesis: o1 = o2
now__::_thesis:_for_x,_y_being_set_st_x_in_Subgroups_G_&_y_in_Subgroups_G_holds_
o1_._(x,y)_=_o2_._(x,y)
let x, y be set ; ::_thesis: ( x in Subgroups G & y in Subgroups G implies o1 . (x,y) = o2 . (x,y) )
assume A5: ( x in Subgroups G & y in Subgroups G ) ; ::_thesis: o1 . (x,y) = o2 . (x,y)
then reconsider A = x, B = y as Element of Subgroups G ;
reconsider H1 = x, H2 = y as strict Subgroup of G by A5, GROUP_3:def_1;
 o1 . (A,B) = H1 "\/" H2 by A3;
hence  o1 . (x,y) = o2 . (x,y) by A4; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:1; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines SubJoin GROUP_4:def_10_:_
 for G being Group
for b2 being BinOp of (Subgroups G) holds
( b2 = SubJoin G iff for H1, H2 being strict Subgroup of G holds b2 . (H1,H2) = H1 "\/" H2 );

definition
let G be Group;
func SubMeet G ->  BinOp of (Subgroups G) means :Def11: :: GROUP_4:def 11
 for H1, H2 being strict Subgroup of G holds it . (H1,H2) = H1 /\ H2;
existence
 ex b1 being BinOp of (Subgroups G) st
for H1, H2 being strict Subgroup of G holds b1 . (H1,H2) = H1 /\ H2
proof
defpred S1[ set , set , set ] means  for H1, H2 being Subgroup of G st $1 = H1 & $2 = H2 holds
$3 = H1 /\ H2;
A1: for S1, S2 being Element of Subgroups G ex B being Element of Subgroups G st S1[S1,S2,B]
proof
let S1, S2 be Element of Subgroups G; ::_thesis: ex B being Element of Subgroups G st S1[S1,S2,B]
reconsider H1 = S1, H2 = S2 as Subgroup of G by GROUP_3:def_1;
reconsider C = H1 /\ H2 as Element of Subgroups G by GROUP_3:def_1;
take  C ; ::_thesis: S1[S1,S2,C]
thus  S1[S1,S2,C] ; ::_thesis: verum
end;
consider o being BinOp of (Subgroups G) such that
A2: for a, b being Element of Subgroups G holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1);
take  o ; ::_thesis: for H1, H2 being strict Subgroup of G holds o . (H1,H2) = H1 /\ H2
let H1, H2 be strict Subgroup of G; ::_thesis: o . (H1,H2) = H1 /\ H2
 ( H1 in Subgroups G & H2 in Subgroups G ) by GROUP_3:def_1;
hence  o . (H1,H2) = H1 /\ H2 by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (Subgroups G) st ( for H1, H2 being strict Subgroup of G holds b1 . (H1,H2) = H1 /\ H2 ) & ( for H1, H2 being strict Subgroup of G holds b2 . (H1,H2) = H1 /\ H2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (Subgroups G); ::_thesis: ( ( for H1, H2 being strict Subgroup of G holds o1 . (H1,H2) = H1 /\ H2 ) & ( for H1, H2 being strict Subgroup of G holds o2 . (H1,H2) = H1 /\ H2 ) implies o1 = o2 )
assume that
A3: for H1, H2 being strict Subgroup of G holds o1 . (H1,H2) = H1 /\ H2 and
A4: for H1, H2 being strict Subgroup of G holds o2 . (H1,H2) = H1 /\ H2 ; ::_thesis: o1 = o2
now__::_thesis:_for_x,_y_being_set_st_x_in_Subgroups_G_&_y_in_Subgroups_G_holds_
o1_._(x,y)_=_o2_._(x,y)
let x, y be set ; ::_thesis: ( x in Subgroups G & y in Subgroups G implies o1 . (x,y) = o2 . (x,y) )
assume A5: ( x in Subgroups G & y in Subgroups G ) ; ::_thesis: o1 . (x,y) = o2 . (x,y)
then reconsider A = x, B = y as Element of Subgroups G ;
reconsider H1 = x, H2 = y as strict Subgroup of G by A5, GROUP_3:def_1;
 o1 . (A,B) = H1 /\ H2 by A3;
hence  o1 . (x,y) = o2 . (x,y) by A4; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:1; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines SubMeet GROUP_4:def_11_:_
 for G being Group
for b2 being BinOp of (Subgroups G) holds
( b2 = SubMeet G iff for H1, H2 being strict Subgroup of G holds b2 . (H1,H2) = H1 /\ H2 );

Lm6:  for G being Group holds
( LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is Lattice & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 0_Lattice & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 1_Lattice )
proof
let G be Group; ::_thesis: ( LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is Lattice & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 0_Lattice & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 1_Lattice )
set L = LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #);
A1: now__::_thesis:_for_A,_B_being_Element_of_LattStr(#_(Subgroups_G),(SubJoin_G),(SubMeet_G)_#)
for_H1,_H2_being_strict_Subgroup_of_G_st_A_=_H1_&_B_=_H2_holds_
A_"\/"_B_=_H1_"\/"_H2
let A, B be Element of LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #); ::_thesis: for H1, H2 being strict Subgroup of G st A = H1 & B = H2 holds
A "\/" B = H1 "\/" H2
let H1, H2 be strict Subgroup of G; ::_thesis: ( A = H1 & B = H2 implies A "\/" B = H1 "\/" H2 )
assume A2: ( A = H1 & B = H2 ) ; ::_thesis: A "\/" B = H1 "\/" H2
thus A "\/" B = (SubJoin G) . (A,B) by LATTICES:def_1
.= H1 "\/" H2 by A2, Def10 ; ::_thesis: verum
end;
A3: now__::_thesis:_for_A,_B_being_Element_of_LattStr(#_(Subgroups_G),(SubJoin_G),(SubMeet_G)_#)
for_H1,_H2_being_strict_Subgroup_of_G_st_A_=_H1_&_B_=_H2_holds_
A_"/\"_B_=_H1_/\_H2
let A, B be Element of LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #); ::_thesis: for H1, H2 being strict Subgroup of G st A = H1 & B = H2 holds
A "/\" B = H1 /\ H2
let H1, H2 be strict Subgroup of G; ::_thesis: ( A = H1 & B = H2 implies A "/\" B = H1 /\ H2 )
assume A4: ( A = H1 & B = H2 ) ; ::_thesis: A "/\" B = H1 /\ H2
thus A "/\" B = (SubMeet G) . (A,B) by LATTICES:def_2
.= H1 /\ H2 by A4, Def11 ; ::_thesis: verum
end;
now__::_thesis:_for_A,_B,_C_being_Element_of_LattStr(#_(Subgroups_G),(SubJoin_G),(SubMeet_G)_#)_holds_
(_A_"\/"_B_=_B_"\/"_A_&_(A_"\/"_B)_"\/"_C_=_A_"\/"_(B_"\/"_C)_&_(A_"/\"_B)_"\/"_B_=_B_&_A_"/\"_B_=_B_"/\"_A_&_(A_"/\"_B)_"/\"_C_=_A_"/\"_(B_"/\"_C)_&_A_"/\"_(A_"\/"_B)_=_A_)
let A, B, C be Element of LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #); ::_thesis: ( A "\/" B = B "\/" A & (A "\/" B) "\/" C = A "\/" (B "\/" C) & (A "/\" B) "\/" B = B & A "/\" B = B "/\" A & (A "/\" B) "/\" C = A "/\" (B "/\" C) & A "/\" (A "\/" B) = A )
reconsider H1 = A, H2 = B, H3 = C as strict Subgroup of G by GROUP_3:def_1;
A5: H2 "\/" H3 = B "\/" C by A1;
thus A "\/" B = H1 "\/" H2 by A1
.= H2 "\/" H1
.= B "\/" A by A1 ; ::_thesis: ( (A "\/" B) "\/" C = A "\/" (B "\/" C) & (A "/\" B) "\/" B = B & A "/\" B = B "/\" A & (A "/\" B) "/\" C = A "/\" (B "/\" C) & A "/\" (A "\/" B) = A )
A6: H1 "\/" H2 = A "\/" B by A1;
hence (A "\/" B) "\/" C = (H1 "\/" H2) "\/" H3 by A1
.= H1 "\/" (H2 "\/" H3) by Th57
.= A "\/" (B "\/" C) by A1, A5 ;
::_thesis: ( (A "/\" B) "\/" B = B & A "/\" B = B "/\" A & (A "/\" B) "/\" C = A "/\" (B "/\" C) & A "/\" (A "\/" B) = A )
A7: H1 /\ H2 = A "/\" B by A3;
hence (A "/\" B) "\/" B = (H1 /\ H2) "\/" H2 by A1
.= B by Th66 ;
::_thesis: ( A "/\" B = B "/\" A & (A "/\" B) "/\" C = A "/\" (B "/\" C) & A "/\" (A "\/" B) = A )
A8: H2 /\ H3 = B "/\" C by A3;
thus A "/\" B = H2 /\ H1 by A3
.= B "/\" A by A3 ; ::_thesis: ( (A "/\" B) "/\" C = A "/\" (B "/\" C) & A "/\" (A "\/" B) = A )
thus (A "/\" B) "/\" C = (H1 /\ H2) /\ H3 by A3, A7
.= H1 /\ (H2 /\ H3) by GROUP_2:84
.= A "/\" (B "/\" C) by A3, A8 ; ::_thesis: A "/\" (A "\/" B) = A
thus A "/\" (A "\/" B) = H1 /\ (H1 "\/" H2) by A3, A6
.= A by Th67 ; ::_thesis: verum
end;
then A9: ( LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is join-commutative & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is join-associative & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is meet-absorbing & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is meet-commutative & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is meet-associative & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is join-absorbing ) by LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence  LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is Lattice ; ::_thesis: ( LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 0_Lattice & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 1_Lattice )
reconsider L = LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) as Lattice by A9;
reconsider E = (1). G as Element of L by GROUP_3:def_1;
now__::_thesis:_for_A_being_Element_of_L_holds_
(_E_"/\"_A_=_E_&_A_"/\"_E_=_E_)
let A be Element of L; ::_thesis: ( E "/\" A = E & A "/\" E = E )
reconsider H = A as strict Subgroup of G by GROUP_3:def_1;
thus E "/\" A = ((1). G) /\ H by A3
.= E by GROUP_2:85 ; ::_thesis: A "/\" E = E
hence  A "/\" E = E ; ::_thesis: verum
end;
hence  LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 0_Lattice by LATTICES:def_13; ::_thesis: LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 1_Lattice
reconsider F = (Omega). G as Element of L by GROUP_3:def_1;
now__::_thesis:_for_A_being_Element_of_L_holds_
(_F_"\/"_A_=_F_&_A_"\/"_F_=_F_)
let A be Element of L; ::_thesis: ( F "\/" A = F & A "\/" F = F )
reconsider H = A as strict Subgroup of G by GROUP_3:def_1;
thus F "\/" A = ((Omega). G) "\/" H by A1
.= F by Th59 ; ::_thesis: A "\/" F = F
hence  A "\/" F = F ; ::_thesis: verum
end;
hence  LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 1_Lattice by LATTICES:def_14; ::_thesis: verum
end;

definition
let G be Group;
func lattice G ->  strict Lattice equals :: GROUP_4:def 12
 LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #);
coherence
 LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is strict Lattice by Lm6;
end;

:: deftheorem  defines lattice GROUP_4:def_12_:_
 for G being Group holds lattice G = LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #);

theorem :: GROUP_4:69
for G being Group holds the carrier of (lattice G) = Subgroups G ;

theorem :: GROUP_4:70
for G being Group holds the L_join of (lattice G) = SubJoin G ;

theorem :: GROUP_4:71
for G being Group holds the L_meet of (lattice G) = SubMeet G ;

registration
let G be Group;
cluster lattice G ->  strict lower-bounded upper-bounded ;
coherence
 ( lattice G is lower-bounded & lattice G is upper-bounded ) by Lm6;
end;

theorem :: GROUP_4:72
for G being Group holds Bottom (lattice G) = (1). G
proof
let G be Group; ::_thesis: Bottom (lattice G) = (1). G
set L = lattice G;
reconsider E = (1). G as Element of (lattice G) by GROUP_3:def_1;
now__::_thesis:_for_A_being_Element_of_(lattice_G)_holds_A_"/\"_E_=_E
let A be Element of (lattice G); ::_thesis: A "/\" E = E
reconsider H = A as strict Subgroup of G by GROUP_3:def_1;
thus A "/\" E = (SubMeet G) . (A,E) by LATTICES:def_2
.= H /\ ((1). G) by Def11
.= E by GROUP_2:85 ; ::_thesis: verum
end;
hence  Bottom (lattice G) = (1). G by RLSUB_2:64; ::_thesis: verum
end;

theorem :: GROUP_4:73
for G being Group holds Top (lattice G) = (Omega). G
proof
let G be Group; ::_thesis: Top (lattice G) = (Omega). G
set L = lattice G;
reconsider E = (Omega). G as Element of (lattice G) by GROUP_3:def_1;
now__::_thesis:_for_A_being_Element_of_(lattice_G)_holds_A_"\/"_E_=_E
let A be Element of (lattice G); ::_thesis: A "\/" E = E
reconsider H = A as strict Subgroup of G by GROUP_3:def_1;
thus A "\/" E = (SubJoin G) . (A,E) by LATTICES:def_1
.= H "\/" ((Omega). G) by Def10
.= E by Th59 ; ::_thesis: verum
end;
hence  Top (lattice G) = (Omega). G by RLSUB_2:65; ::_thesis: verum
end;