GROUP_8

:: GROUP_8 semantic presentation

begin

for p being ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )
for G being ( ( non empty finite strict Group-like V109() ) ( non empty finite strict unital Group-like V109() ) Group) st p : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) is prime & card G : ( ( non empty finite strict Group-like V109() ) ( non empty finite strict unital Group-like V109() ) Group) : ( ( ) ( V6() V7() V8() V12() non empty V31() V32() integer cardinal ext-real positive non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = p : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
ex a being ( ( ) ( ) Element of ( ( ) ( non empty finite ) set ) ) st ord a : ( ( ) ( ) Element of ( ( ) ( non empty finite ) set ) ) : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = p : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: GROUP_8:2

for G being ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group)
for H being ( ( ) ( non empty unital Group-like V109() ) Subgroup of G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) )
for a1, a2 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for b1, b2 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * a2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) : ( ( ) ( non empty ) set ) ) = b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) ;

theorem :: GROUP_8:3

for G being ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group)
for H being ( ( ) ( non empty unital Group-like V109() ) Subgroup of G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
for n being ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ n : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) : ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ n : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) ;

theorem :: GROUP_8:4

for G being ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group)
for H being ( ( ) ( non empty unital Group-like V109() ) Subgroup of G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
for i being ( ( integer ) ( V31() V32() integer ext-real ) Integer) holds a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ i : ( ( integer ) ( V31() V32() integer ext-real ) Integer) : ( ( ) ( ) Element of the carrier of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) : ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ i : ( ( integer ) ( V31() V32() integer ext-real ) Integer) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) ;

theorem :: GROUP_8:5

theorem :: GROUP_8:6

theorem :: GROUP_8:7

for G being ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> 1_ G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non being_of_order_0 ) Element of the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) holds
gr {a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of bool the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) <> (1). G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( strict ) ( non empty finite strict unital Group-like V109() V111() cyclic ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ;

theorem :: GROUP_8:8

for G being ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group)
for m being ( ( integer ) ( V31() V32() integer ext-real ) Integer) holds (1_ G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) : ( ( ) ( non being_of_order_0 ) Element of the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) |^ m : ( ( integer ) ( V31() V32() integer ext-real ) Integer) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) = 1_ G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non being_of_order_0 ) Element of the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) ;

theorem :: GROUP_8:9

for G being ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for m being ( ( integer ) ( V31() V32() integer ext-real ) Integer) holds a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ (m : ( ( integer ) ( V31() V32() integer ext-real ) Integer) * (ord a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V31() V32() integer ext-real ) set ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) = 1_ G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non being_of_order_0 ) Element of the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) ;

theorem :: GROUP_8:10

for G being ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_of_order_0 holds
for m being ( ( integer ) ( V31() V32() integer ext-real ) Integer) holds a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ m : ( ( integer ) ( V31() V32() integer ext-real ) Integer) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ (m : ( ( integer ) ( V31() V32() integer ext-real ) Integer) mod (ord a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( integer ) ( V31() V32() integer ext-real ) set ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) ;

theorem :: GROUP_8:11

for G being ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group)
for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_of_order_0 holds
gr {b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of bool the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) is finite ;

theorem :: GROUP_8:12

for G being ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group)
for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_of_order_0 holds
b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) " : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) is being_of_order_0 ;

theorem :: GROUP_8:13

for G being ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group)
for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_of_order_0 iff for n being ( ( integer ) ( V31() V32() integer ext-real ) Integer) st b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ n : ( ( integer ) ( V31() V32() integer ext-real ) Integer) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) = 1_ G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non being_of_order_0 ) Element of the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) holds
n : ( ( integer ) ( V31() V32() integer ext-real ) Integer) = 0 : ( ( ) ( V6() V7() V8() V10() V11() V12() functional empty V31() V32() integer finite V40() FinSequence-membered ext-real non positive non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GROUP_8:14

for G being ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) st ex a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) <> 1_ G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non being_of_order_0 ) Element of the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) holds
( ( for H being ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) holds
( H : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) or H : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = (1). G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( strict ) ( non empty finite strict unital Group-like V109() V111() cyclic ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) ) ) iff ( G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) is cyclic & G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) is finite & ex p being ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st
( card G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( cardinal ) ( cardinal ) set ) = p : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & p : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) is prime ) ) ) ;

theorem :: GROUP_8:15

for G being ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group)
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) holds
( z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) iff ex a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) ) ) ;

theorem :: GROUP_8:16

for G being ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group)
for A being ( ( non empty ) ( non empty ) Subset of )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds card A : ( ( non empty ) ( non empty ) Subset of ) : ( ( cardinal ) ( cardinal ) set ) = card (((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ") : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) * A : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( cardinal ) ( cardinal ) set ) ;

definition

let G be ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ;
let H, K be ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) ;

func Double_Cosets (H,K) -> ( ( ) ( ) Subset-Family of ) means :: GROUP_8:def 1
for A being ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) in it : ( ( ) ( ) Element of G : ( ( ) ( ) doubleLoopStr ) ) iff ex a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st A : ( ( ) ( ) Subset of ) = (H : ( ( Function-like V25([:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) ) ( Relation-like [:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like V25([:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) ) Element of bool [:[:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) * K : ( ( Function-like V25([:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) ) ( Relation-like [:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( ) set ) -defined G : ( ( ) ( ) doubleLoopStr ) -valued Function-like V25([:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) ) ) Element of bool [:[:G : ( ( ) ( ) doubleLoopStr ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,G : ( ( ) ( ) doubleLoopStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of G : ( ( ) ( ) doubleLoopStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) );

end;

theorem :: GROUP_8:17

for G being ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group)
for z, x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for H, K being ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) holds
( z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in (H : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) * K : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) iff ex g, h being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) * h : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) & g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in H : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) & h : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in K : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) ) ) ;

theorem :: GROUP_8:18

for G being ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for H, K being ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) holds
( (H : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) * K : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = (H : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) * K : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) or for z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( not z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in (H : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) * x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) * K : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) or not z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in (H : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) * K : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

registration

let G be ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ;
let A be ( ( ) ( non empty unital Group-like V109() ) Subgroup of G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ;

cluster Left_Cosets A : ( ( ) ( non empty unital Group-like V109() ) Subgroup of G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) multMagma ) ) : ( ( ) ( ) Element of bool (bool the carrier of G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) multMagma ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -> non empty ;

end;

notation

let G be ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ;
let H be ( ( ) ( non empty unital Group-like V109() ) Subgroup of G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ;
synonym index (G,H) for index H;

end;

theorem :: GROUP_8:19

for G being ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group)
for A, B being ( ( ) ( non empty unital Group-like V109() ) Subgroup of G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) )
for D being ( ( ) ( non empty unital Group-like V109() ) Subgroup of A : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) st D : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) = A : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) /\ B : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) & G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) is finite holds
index (G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ,B : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) >= index (A : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ,D : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) ) : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: GROUP_8:20

for G being ( ( non empty finite Group-like V109() ) ( non empty finite unital Group-like V109() ) Group)
for H being ( ( ) ( non empty finite unital Group-like V109() ) Subgroup of G : ( ( non empty finite Group-like V109() ) ( non empty finite unital Group-like V109() ) Group) ) holds index (G : ( ( non empty finite Group-like V109() ) ( non empty finite unital Group-like V109() ) Group) ,H : ( ( ) ( non empty finite unital Group-like V109() ) Subgroup of b₁ : ( ( non empty finite Group-like V109() ) ( non empty finite unital Group-like V109() ) Group) ) ) : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) > 0 : ( ( ) ( V6() V7() V8() V10() V11() V12() functional empty V31() V32() integer finite V40() FinSequence-membered ext-real non positive non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: GROUP_8:21

for G being ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) st G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) is finite holds
for C being ( ( ) ( non empty unital Group-like V109() ) Subgroup of G : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) )
for A, B being ( ( ) ( non empty unital Group-like V109() ) Subgroup of C : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) )
for D being ( ( ) ( non empty unital Group-like V109() ) Subgroup of A : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) ) st D : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₃ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) ) = A : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) /\ B : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) holds
for E being ( ( ) ( non empty unital Group-like V109() ) Subgroup of B : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) ) st E : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₄ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) ) = A : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) /\ B : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) holds
for F being ( ( ) ( non empty unital Group-like V109() ) Subgroup of C : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) st F : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) = A : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) /\ B : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) & index (C : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ,A : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) ) : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) , index (C : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ,B : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) ) : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) are_relative_prime holds
( index (C : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ,B : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) ) : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = index (A : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) ,D : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₃ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) ) ) : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & index (C : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ,A : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) ) : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = index (B : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) ,E : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₄ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₂ : ( ( ) ( non empty unital Group-like V109() ) Subgroup of b₁ : ( ( non empty Group-like V109() ) ( non empty unital Group-like V109() ) Group) ) ) ) ) : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GROUP_8:22

theorem :: GROUP_8:23

for G being ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) st G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) <> (1). G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( strict ) ( non empty finite strict unital Group-like V109() V111() cyclic ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) holds
ex b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> 1_ G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non being_of_order_0 ) Element of the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) ;

theorem :: GROUP_8:24

for G being ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) = gr {a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of bool the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) holds
for H being ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) st H : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) <> (1). G : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( strict ) ( non empty finite strict unital Group-like V109() V111() cyclic ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) holds
ex k being ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st
( 0 : ( ( ) ( V6() V7() V8() V10() V11() V12() functional empty V31() V32() integer finite V40() FinSequence-membered ext-real non positive non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) < k : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) |^ k : ( ( ) ( V6() V7() V8() V12() V31() V32() integer ext-real non negative ) Element of NAT : ( ( ) ( V6() V7() V8() non empty ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) : ( ( ) ( non empty ) set ) ) in H : ( ( strict ) ( non empty strict unital Group-like V109() ) Subgroup of b₁ : ( ( non empty strict Group-like V109() ) ( non empty strict unital Group-like V109() ) Group) ) ) ;

theorem :: GROUP_8:25