:: GR_CY_2 semantic presentation
begin
theorem
:: GR_CY_2:1
for
G
being ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
)
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
for
k
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) st
ord
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) ) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
>
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
|^
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
) ) holds
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
<>
0
: ( ( ) (
functional
zero
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
V32
()
integer
V39
()
V43
()
FinSequence-membered
ext-real
non
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
set
) ;
theorem
:: GR_CY_2:2
for
G
being ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
in
gr
{
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) ) : ( (
strict
) (
V60
()
strict
unital
Group-like
V133
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ) ;
theorem
:: GR_CY_2:3
for
G
being ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
)
for
G1
being ( ( ) (
V60
()
unital
Group-like
V133
() )
Subgroup
of
G
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) )
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
for
a1
being ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
=
a1
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) ) holds
gr
{
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) ) : ( (
strict
) (
V60
()
strict
unital
Group-like
V133
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) )
=
gr
{
a1
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
2
: ( ( ) (
V60
()
unital
Group-like
V133
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) ) : ( (
strict
) (
V60
()
strict
unital
Group-like
V133
() )
Subgroup
of
b
2
: ( ( ) (
V60
()
unital
Group-like
V133
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ) ) ;
theorem
:: GR_CY_2:4
for
G
being ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) ) holds
gr
{
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) ) : ( (
strict
) (
V60
()
strict
unital
Group-like
V133
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ) is ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ;
theorem
:: GR_CY_2:5
for
G
being ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
)
for
b
being ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) ) holds
( ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) ) ex
i
being ( (
integer
) (
complex
V32
()
integer
ext-real
)
Integer
) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
|^
i
: ( (
integer
) (
complex
V32
()
integer
ext-real
)
Integer
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
) ) ) iff
G
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
)
=
gr
{
b
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
1
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) ) : ( (
strict
) (
V60
()
strict
unital
Group-like
V133
() )
Subgroup
of
b
1
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) ) ) ;
theorem
:: GR_CY_2:6
for
G
being ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
)
for
b
being ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) ) holds
( ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) ) ex
p
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) st
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
|^
p
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) ) ) iff
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
)
=
gr
{
b
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
1
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) ( )
set
) ) : ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
1
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) ) ) ;
theorem
:: GR_CY_2:7
for
G
being ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) ) st
G
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) is
finite
&
G
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
)
=
gr
{
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
1
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) ) : ( (
strict
) (
V60
()
strict
unital
Group-like
V133
() )
Subgroup
of
b
1
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) ) holds
for
G1
being ( (
strict
) (
V60
()
strict
unital
Group-like
V133
() )
Subgroup
of
G
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) ) ex
p
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) st
G1
: ( (
strict
) (
V60
()
strict
unital
Group-like
V133
() )
Subgroup
of
b
1
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) )
=
gr
{
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
|^
p
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
1
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) ) : ( (
strict
) (
V60
()
strict
unital
Group-like
V133
() )
Subgroup
of
b
1
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) ) ;
theorem
:: GR_CY_2:8
for
n
,
p
,
s
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
for
G
being ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) ) st
G
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
)
=
gr
{
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
4
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) (
V39
()
V43
() )
set
) ) : ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
4
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) ) &
card
G
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) &
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
p
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
*
s
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
ext-real
non
negative
)
set
) holds
ord
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
|^
p
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
4
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
s
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: GR_CY_2:9
for
G
being ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
for
s
,
k
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) st
s
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
divides
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
|^
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
) )
in
gr
{
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
|^
s
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) ) : ( (
strict
) (
V60
()
strict
unital
Group-like
V133
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ) ;
theorem
:: GR_CY_2:10
for
s
,
k
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
for
G
being ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) ) st
card
(
gr
{
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
|^
s
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) (
V39
()
V43
() )
set
) )
)
: ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) ) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
card
(
gr
{
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
|^
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) (
V39
()
V43
() )
set
) )
)
: ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) ) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
|^
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of the
carrier
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) )
in
gr
{
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
|^
s
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) (
V39
()
V43
() )
set
) ) : ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) ) holds
gr
{
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
|^
s
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) (
V39
()
V43
() )
set
) ) : ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) )
=
gr
{
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
|^
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) (
V39
()
V43
() )
set
) ) : ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
3
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) ) ;
theorem
:: GR_CY_2:11
for
n
,
p
,
k
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
for
G
being ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
)
for
G1
being ( ( ) (
V60
()
finite
unital
Group-like
V133
() )
Subgroup
of
G
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) )
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) ) st
card
G
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) &
G
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
)
=
gr
{
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
4
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) (
V39
()
V43
() )
set
) ) : ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
4
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) ) &
card
G1
: ( ( ) (
V60
()
finite
unital
Group-like
V133
() )
Subgroup
of
b
4
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) ) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
p
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) &
G1
: ( ( ) (
V60
()
finite
unital
Group-like
V133
() )
Subgroup
of
b
4
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) )
=
gr
{
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
|^
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
4
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
4
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) (
V39
()
V43
() )
set
) ) : ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
4
: ( (
V60
()
finite
Group-like
V133
() ) (
V60
()
finite
unital
Group-like
V133
() )
Group
) ) holds
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
divides
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
*
p
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
ext-real
non
negative
)
set
) ;
theorem
:: GR_CY_2:12
for
n
,
k
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
for
G
being ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) ) st
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
)
=
gr
{
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
3
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) (
V39
()
V43
() )
set
) ) : ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
3
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) ) &
card
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
)
=
gr
{
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
|^
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
3
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
3
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) (
V39
()
V43
() )
set
) ) : ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
3
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) ) iff
k
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
gcd
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
1 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: GR_CY_2:13
for
Gc
being ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
)
for
H
being ( ( ) (
V60
()
unital
Group-like
V133
()
V135
() )
Subgroup
of
Gc
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) )
for
g
being ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) ) st
Gc
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
)
=
gr
{
g
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) ) : ( (
strict
) (
V60
()
strict
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) &
g
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
in
H
: ( ( ) (
V60
()
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) holds
multMagma
(# the
carrier
of
Gc
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
) , the
multF
of
Gc
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( (
Function-like
quasi_total
) (
Relation-like
K20
( the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
) , the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
)
-valued
Function-like
quasi_total
V22
( the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
) ) )
Element
of
K19
(
K20
(
K20
( the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
) , the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) , the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
unital
Group-like
V133
() )
multMagma
)
=
multMagma
(# the
carrier
of
H
: ( ( ) (
V60
()
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) : ( ( ) ( non
zero
)
set
) , the
multF
of
H
: ( ( ) (
V60
()
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) : ( (
Function-like
quasi_total
) (
Relation-like
K20
( the
carrier
of
b
2
: ( ( ) (
V60
()
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) : ( ( ) ( non
zero
)
set
) , the
carrier
of
b
2
: ( ( ) (
V60
()
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
2
: ( ( ) (
V60
()
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) : ( ( ) ( non
zero
)
set
)
-valued
Function-like
quasi_total
V22
( the
carrier
of
b
2
: ( ( ) (
V60
()
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) : ( ( ) ( non
zero
)
set
) ) )
Element
of
K19
(
K20
(
K20
( the
carrier
of
b
2
: ( ( ) (
V60
()
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) : ( ( ) ( non
zero
)
set
) , the
carrier
of
b
2
: ( ( ) (
V60
()
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) , the
carrier
of
b
2
: ( ( ) (
V60
()
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) #) : ( (
strict
) (
strict
unital
Group-like
V133
() )
multMagma
) ;
theorem
:: GR_CY_2:14
for
Gc
being ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
)
for
g
being ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) ) st
Gc
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
)
=
gr
{
g
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) ) : ( (
strict
) (
V60
()
strict
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) holds
(
Gc
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) is
finite
iff ex
i
,
i1
being ( (
integer
) (
complex
V32
()
integer
ext-real
)
Integer
) st
(
i
: ( (
integer
) (
complex
V32
()
integer
ext-real
)
Integer
)
<>
i1
: ( (
integer
) (
complex
V32
()
integer
ext-real
)
Integer
) &
g
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
|^
i
: ( (
integer
) (
complex
V32
()
integer
ext-real
)
Integer
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
) )
=
g
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
|^
i1
: ( (
integer
) (
complex
V32
()
integer
ext-real
)
Integer
) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
) ) ) ) ;
registration
let
n
be ( ( non
zero
natural
) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
ext-real
positive
non
negative
)
Nat
) ;
cluster
->
natural
for ( ( ) ( )
Element
of the
carrier
of
(
INT.Group
n
: ( ( ) ( )
doubleLoopStr
)
)
: ( (
V60
()
strict
) (
V60
()
strict
)
multMagma
) : ( ( ) ( non
zero
)
set
) ) ;
end;
theorem
:: GR_CY_2:15
for
Gc
being ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) holds
INT.Group
(
card
Gc
: ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
)
)
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
V60
()
strict
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
multMagma
) ,
Gc
: ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
)
are_isomorphic
;
theorem
:: GR_CY_2:16
for
Gc
being ( (
V60
()
strict
Group-like
V133
()
cyclic
) (
V60
()
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) st
Gc
: ( (
V60
()
strict
Group-like
V133
()
cyclic
) (
V60
()
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) is
infinite
holds
INT.Group
: ( (
V60
()
strict
) (
V60
()
strict
unital
Group-like
V133
()
V135
()
cyclic
)
multMagma
) ,
Gc
: ( (
V60
()
strict
Group-like
V133
()
cyclic
) (
V60
()
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
)
are_isomorphic
;
theorem
:: GR_CY_2:17
for
Gc
,
Hc
being ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) st
card
Hc
: ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
card
Gc
: ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
Hc
: ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ,
Gc
: ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
)
are_isomorphic
;
theorem
:: GR_CY_2:18
for
p
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
for
F
,
G
being ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) st
card
F
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
p
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) &
card
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
p
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) &
p
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) is
prime
holds
F
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) ,
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
)
are_isomorphic
;
theorem
:: GR_CY_2:19
for
F
,
G
being ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) st
card
F
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) &
card
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
F
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) ,
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
)
are_isomorphic
;
theorem
:: GR_CY_2:20
for
G
being ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) st
card
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
for
H
being ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) ) holds
(
H
: ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
1
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) )
=
(1).
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) : ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Subgroup
of
b
1
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) ) or
H
: ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
1
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) )
=
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) ) ;
theorem
:: GR_CY_2:21
for
G
being ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) st
card
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) is ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ;
theorem
:: GR_CY_2:22
for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
for
G
being ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) st
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) is
cyclic
&
card
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
for
p
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) st
p
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
divides
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
ex
G1
being ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) ) st
(
card
G1
: ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
2
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) ) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
p
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) & ( for
G2
being ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
G
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) ) st
card
G2
: ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
2
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) ) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
p
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
G2
: ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
2
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) )
=
G1
: ( (
strict
) (
V60
()
finite
strict
unital
Group-like
V133
() )
Subgroup
of
b
2
: ( (
V60
()
finite
strict
Group-like
V133
() ) (
V60
()
finite
strict
unital
Group-like
V133
() )
Group
) ) ) ) ;
theorem
:: GR_CY_2:23
for
Gc
being ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
)
for
g
being ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) ) st
Gc
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
)
=
gr
{
g
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
}
: ( ( ) ( non
zero
V39
() )
Element
of
K19
( the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
) ) : ( ( ) ( )
set
) ) : ( (
strict
) (
V60
()
strict
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) holds
for
G
being ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
)
for
f
being ( (
Function-like
quasi_total
V140
(
b
3
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ,
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) ) (
Relation-like
the
carrier
of
b
3
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
)
-defined
the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
)
-valued
Function-like
quasi_total
V140
(
b
3
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ,
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) )
Homomorphism
of
G
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ,
Gc
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) st
g
: ( ( ) ( )
Element
of ( ( ) ( non
zero
)
set
) )
in
Image
f
: ( (
Function-like
quasi_total
V140
(
b
3
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ,
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) ) (
Relation-like
the
carrier
of
b
3
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
)
-defined
the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
)
-valued
Function-like
quasi_total
V140
(
b
3
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ,
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) )
Homomorphism
of
b
3
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ,
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) : ( (
strict
) (
V60
()
strict
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) holds
f
: ( (
Function-like
quasi_total
V140
(
b
3
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ,
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) ) (
Relation-like
the
carrier
of
b
3
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
)
-defined
the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
)
set
)
-valued
Function-like
quasi_total
V140
(
b
3
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ,
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) )
Homomorphism
of
b
3
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ,
b
1
: ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) is
onto
;
theorem
:: GR_CY_2:24
for
Gc
being ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) st ex
k
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) st
card
Gc
: ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
*
k
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) ( )
set
) holds
ex
g1
being ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) ) st
(
ord
g1
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) & ( for
g2
being ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) ) st
ord
g2
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) ) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
g1
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) )
=
g2
: ( ( ) ( )
Element
of ( ( ) ( non
zero
V39
() )
set
) ) ) ) ;
registration
let
G
be ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ;
cluster
center
G
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
multMagma
) : ( (
strict
) (
V60
()
strict
unital
Group-like
V133
() )
Subgroup
of
G
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
multMagma
) )
->
strict
normal
;
end;
theorem
:: GR_CY_2:25
for
Gc
being ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) st ex
k
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) st
card
Gc
: ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
*
k
: ( ( ) (
V60
()
finite
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) : ( ( ) ( )
set
) holds
ex
H
being ( ( ) (
V60
()
finite
unital
Group-like
V133
()
V135
() )
Subgroup
of
Gc
: ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) st
(
card
H
: ( ( ) (
V60
()
finite
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
cardinal
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) )
=
2 : ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
natural
complex
V32
()
integer
V35
()
ext-real
positive
non
negative
V154
()
V155
()
V156
()
V157
()
V158
()
V159
() )
Element
of
NAT
: ( ( ) ( non
zero
epsilon-transitive
epsilon-connected
ordinal
V154
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
() )
Element
of
K19
(
REAL
: ( ( ) (
V154
()
V155
()
V156
()
V160
() )
set
) ) : ( ( ) ( )
set
) ) ) &
H
: ( ( ) (
V60
()
finite
unital
Group-like
V133
()
V135
() )
Subgroup
of
b
1
: ( (
V60
()
finite
strict
Group-like
V133
()
cyclic
) (
V60
()
finite
strict
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) is ( (
V60
()
Group-like
V133
()
cyclic
) (
V60
()
unital
Group-like
V133
()
V135
()
cyclic
)
Group
) ) ;
theorem
:: GR_CY_2:26
for
F
being ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
)
for
G
being ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
)
for
g
being ( (
Function-like
quasi_total
V140
(
b
2
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) ,
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ) ) (
Relation-like
the
carrier
of
b
2
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
)
-defined
the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
)
-valued
Function-like
quasi_total
V140
(
b
2
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) ,
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ) )
Homomorphism
of
G
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) ,
F
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ) st
G
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) is
cyclic
holds
Image
g
: ( (
Function-like
quasi_total
V140
(
b
2
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) ,
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ) ) (
Relation-like
the
carrier
of
b
2
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
)
-defined
the
carrier
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) : ( ( ) ( non
zero
)
set
)
-valued
Function-like
quasi_total
V140
(
b
2
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) ,
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ) )
Homomorphism
of
b
2
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) ,
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ) : ( (
strict
) (
V60
()
strict
unital
Group-like
V133
() )
Subgroup
of
b
1
: ( (
V60
()
Group-like
V133
() ) (
V60
()
unital
Group-like
V133
() )
Group
) ) is
cyclic
;
theorem
:: GR_CY_2:27
for
G
,
F
being ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) st
G
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) ,
F
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
)
are_isomorphic
&
G
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) is
cyclic
holds
F
: ( (
V60
()
strict
Group-like
V133
() ) (
V60
()
strict
unital
Group-like
V133
() )
Group
) is
cyclic
;