:: GR_CY_2 semantic presentation

REAL is V154() V155() V156() V160() set

NAT is non zero epsilon-transitive epsilon-connected ordinal V154() V155() V156() V157() V158() V159() V160() Element of K19(REAL)

K19(REAL) is set

COMPLEX is V154() V160() set

RAT is V154() V155() V156() V157() V160() set

INT is V154() V155() V156() V157() V158() V160() set

K20(COMPLEX,COMPLEX) is set

K19(K20(COMPLEX,COMPLEX)) is set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set

K20(REAL,REAL) is set

K19(K20(REAL,REAL)) is set

K20(K20(REAL,REAL),REAL) is set

K19(K20(K20(REAL,REAL),REAL)) is set

K20(RAT,RAT) is set

K19(K20(RAT,RAT)) is set

K20(K20(RAT,RAT),RAT) is set

K19(K20(K20(RAT,RAT),RAT)) is set

K20(INT,INT) is set

K19(K20(INT,INT)) is set

K20(K20(INT,INT),INT) is set

K19(K20(K20(INT,INT),INT)) is set

K20(NAT,NAT) is set

K20(K20(NAT,NAT),NAT) is set

K19(K20(K20(NAT,NAT),NAT)) is set

omega is non zero epsilon-transitive epsilon-connected ordinal V154() V155() V156() V157() V158() V159() V160() set

K19(omega) is set

K19(NAT) is set

INT.Group is V60() strict unital Group-like V133() V135() cyclic multMagma

K222() is Relation-like K20(INT,INT) -defined INT -valued Function-like quasi_total Element of K19(K20(K20(INT,INT),INT))

multMagma(# INT,K222() #) is strict multMagma

the carrier of INT.Group is non zero V154() V155() V156() V157() V158() set

0 is 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

1 is 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

2 is 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

3 is 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

0 is functional zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V32() integer V35() V39() V43() FinSequence-membered ext-real non positive non negative V154() V155() V156() V157() V158() V159() V160() Element of NAT

G is V60() unital Group-like V133() multMagma

the carrier of G is non zero set

F is Element of the carrier of G

ord F is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

h is Element of the carrier of G

a is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

h |^ a is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

G is V60() unital Group-like V133() multMagma

the carrier of G is non zero set

F is Element of the carrier of G

{F} is non zero V39() Element of K19( the carrier of G)

K19( the carrier of G) is set

gr {F} is V60() strict unital Group-like V133() Subgroup of G

h is complex V32() integer ext-real set

F |^ h is Element of the carrier of G

h is complex V32() integer ext-real set

F |^ h is Element of the carrier of G

G is V60() unital Group-like V133() multMagma

the carrier of G is non zero set

F is V60() unital Group-like V133() Subgroup of G

the carrier of F is non zero set

h is Element of the carrier of G

{h} is non zero V39() Element of K19( the carrier of G)

K19( the carrier of G) is set

gr {h} is V60() strict unital Group-like V133() Subgroup of G

a is Element of the carrier of F

{a} is non zero V39() Element of K19( the carrier of F)

K19( the carrier of F) is set

gr {a} is V60() strict unital Group-like V133() Subgroup of F

f is V60() unital Group-like V133() Subgroup of G

d is Element of the carrier of G

b is Element of the carrier of F

i is complex V32() integer ext-real set

a |^ i is Element of the carrier of F

h |^ i is Element of the carrier of G

d is Element of the carrier of G

b is complex V32() integer ext-real set

h |^ b is Element of the carrier of G

a |^ b is Element of the carrier of F

G is V60() unital Group-like V133() multMagma

the carrier of G is non zero set

F is Element of the carrier of G

{F} is non zero V39() Element of K19( the carrier of G)

K19( the carrier of G) is set

gr {F} is V60() strict unital Group-like V133() Subgroup of G

the carrier of (gr {F}) is non zero set

h is Element of the carrier of (gr {F})

{h} is non zero V39() Element of K19( the carrier of (gr {F}))

K19( the carrier of (gr {F})) is set

gr {h} is V60() strict unital Group-like V133() Subgroup of gr {F}

h is Element of the carrier of (gr {F})

{h} is non zero V39() Element of K19( the carrier of (gr {F}))

K19( the carrier of (gr {F})) is set

gr {h} is V60() strict unital Group-like V133() Subgroup of gr {F}

G is V60() strict unital Group-like V133() multMagma

the carrier of G is non zero set

F is Element of the carrier of G

{F} is non zero V39() Element of K19( the carrier of G)

K19( the carrier of G) is set

gr {F} is V60() strict unital Group-like V133() Subgroup of G

h is Element of the carrier of G

a is complex V32() integer ext-real set

F |^ a is Element of the carrier of G

h is Element of the carrier of G

G is V60() finite strict unital Group-like V133() multMagma

the carrier of G is non zero V39() set

F is Element of the carrier of G

{F} is non zero V39() Element of K19( the carrier of G)

K19( the carrier of G) is V39() V43() set

gr {F} is V60() finite strict unital Group-like V133() Subgroup of G

card G is 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

a is Element of the carrier of G

f is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F |^ f is Element of the carrier of G

d is complex V32() integer ext-real set

F |^ d is Element of the carrier of G

a is Element of the carrier of G

f is complex V32() integer ext-real set

F |^ f is Element of the carrier of G

h is complex V32() integer ext-real set

f mod h is complex V32() integer ext-real set

d is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F |^ d is Element of the carrier of G

f div h is complex V32() integer ext-real set

(f div h) * h is complex V32() integer ext-real set

((f div h) * h) + (f mod h) is complex V32() integer ext-real set

F |^ (((f div h) * h) + (f mod h)) is Element of the carrier of G

F |^ ((f div h) * h) is Element of the carrier of G

F |^ (f mod h) is Element of the carrier of G

(F |^ ((f div h) * h)) * (F |^ (f mod h)) is Element of the carrier of G

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total V22( the carrier of G) V39() Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is V39() set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is V39() set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is V39() V43() set

K84( the carrier of G, the multF of G,(F |^ ((f div h) * h)),(F |^ (f mod h))) is Element of the carrier of G

F |^ (f div h) is Element of the carrier of G

(F |^ (f div h)) |^ (card G) is Element of the carrier of G

((F |^ (f div h)) |^ (card G)) * (F |^ (f mod h)) is Element of the carrier of G

K84( the carrier of G, the multF of G,((F |^ (f div h)) |^ (card G)),(F |^ (f mod h))) is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

(1_ G) * (F |^ (f mod h)) is Element of the carrier of G

K84( the carrier of G, the multF of G,(1_ G),(F |^ (f mod h))) is Element of the carrier of G

G is V60() strict unital Group-like V133() multMagma

the carrier of G is non zero set

F is Element of the carrier of G

{F} is non zero V39() Element of K19( the carrier of G)

K19( the carrier of G) is set

gr {F} is V60() strict unital Group-like V133() Subgroup of G

h is V60() strict unital Group-like V133() Subgroup of G

the carrier of h is non zero set

a is Element of the carrier of h

{a} is non zero V39() Element of K19( the carrier of h)

K19( the carrier of h) is set

gr {a} is V60() strict unital Group-like V133() Subgroup of h

f is Element of the carrier of G

d is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F |^ d is Element of the carrier of G

{(F |^ d)} is non zero V39() Element of K19( the carrier of G)

gr {(F |^ d)} is V60() strict unital Group-like V133() Subgroup of G

G is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

h is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F * h is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

a is V60() finite unital Group-like V133() multMagma

the carrier of a is non zero V39() set

card a is 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

f is Element of the carrier of a

{f} is non zero V39() Element of K19( the carrier of a)

K19( the carrier of a) is V39() V43() set

gr {f} is V60() finite strict unital Group-like V133() Subgroup of a

f |^ F is Element of the carrier of a

ord (f |^ F) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

1_ a is non being_of_order_0 Element of the carrier of a

d is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

(f |^ F) |^ d is Element of the carrier of a

F * d is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

f |^ (F * d) is Element of the carrier of a

ord f is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

(f |^ F) |^ h is Element of the carrier of a

f |^ G is Element of the carrier of a

G is V60() unital Group-like V133() multMagma

the carrier of G is non zero set

F is Element of the carrier of G

h is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F |^ h is Element of the carrier of G

{(F |^ h)} is non zero V39() Element of K19( the carrier of G)

K19( the carrier of G) is set

gr {(F |^ h)} is V60() strict unital Group-like V133() Subgroup of G

a is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F |^ a is Element of the carrier of G

f is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

h * f is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

d is complex V32() integer ext-real set

(F |^ h) |^ d is Element of the carrier of G

d is complex V32() integer ext-real set

(F |^ h) |^ d is Element of the carrier of G

G is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

h is V60() finite unital Group-like V133() multMagma

the carrier of h is non zero V39() set

a is Element of the carrier of h

a |^ G is Element of the carrier of h

{(a |^ G)} is non zero V39() Element of K19( the carrier of h)

K19( the carrier of h) is V39() V43() set

gr {(a |^ G)} is V60() finite strict unital Group-like V133() Subgroup of h

card (gr {(a |^ G)}) is 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

a |^ F is Element of the carrier of h

{(a |^ F)} is non zero V39() Element of K19( the carrier of h)

gr {(a |^ F)} is V60() finite strict unital Group-like V133() Subgroup of h

card (gr {(a |^ F)}) is 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

the carrier of (gr {(a |^ G)}) is non zero V39() set

f is Element of the carrier of (gr {(a |^ G)})

{f} is non zero V39() Element of K19( the carrier of (gr {(a |^ G)}))

K19( the carrier of (gr {(a |^ G)})) is V39() V43() set

gr {f} is V60() finite strict unital Group-like V133() Subgroup of gr {(a |^ G)}

card (gr {f}) is 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

G is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

h is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

h * F is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

a is V60() finite unital Group-like V133() multMagma

the carrier of a is non zero V39() set

card a is 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

f is V60() finite unital Group-like V133() Subgroup of a

card f is 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

d is Element of the carrier of a

{d} is non zero V39() Element of K19( the carrier of a)

K19( the carrier of a) is V39() V43() set

gr {d} is V60() finite strict unital Group-like V133() Subgroup of a

d |^ h is Element of the carrier of a

{(d |^ h)} is non zero V39() Element of K19( the carrier of a)

gr {(d |^ h)} is V60() finite strict unital Group-like V133() Subgroup of a

i is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

G * i is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

c

(G * i) + c

the carrier of f is non zero V39() set

d |^ (h * F) is Element of the carrier of a

(d |^ h) |^ F is Element of the carrier of a

m is Element of the carrier of f

m |^ F is Element of the carrier of f

1_ f is non being_of_order_0 Element of the carrier of f

1_ a is non being_of_order_0 Element of the carrier of a

d |^ (G * i) is Element of the carrier of a

d |^ c

(d |^ (G * i)) * (d |^ c

the multF of a is Relation-like K20( the carrier of a, the carrier of a) -defined the carrier of a -valued Function-like quasi_total V22( the carrier of a) V39() Element of K19(K20(K20( the carrier of a, the carrier of a), the carrier of a))

K20( the carrier of a, the carrier of a) is V39() set

K20(K20( the carrier of a, the carrier of a), the carrier of a) is V39() set

K19(K20(K20( the carrier of a, the carrier of a), the carrier of a)) is V39() V43() set

K84( the carrier of a, the multF of a,(d |^ (G * i)),(d |^ c

d |^ G is Element of the carrier of a

(d |^ G) |^ i is Element of the carrier of a

((d |^ G) |^ i) * (d |^ c

K84( the carrier of a, the multF of a,((d |^ G) |^ i),(d |^ c

(1_ a) |^ i is Element of the carrier of a

((1_ a) |^ i) * (d |^ c

K84( the carrier of a, the multF of a,((1_ a) |^ i),(d |^ c

(1_ a) * (d |^ c

K84( the carrier of a, the multF of a,(1_ a),(d |^ c

ord d is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

G is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F gcd G is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

h is V60() finite strict unital Group-like V133() multMagma

the carrier of h is non zero V39() set

card h is 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

a is Element of the carrier of h

{a} is non zero V39() Element of K19( the carrier of h)

K19( the carrier of h) is V39() V43() set

gr {a} is V60() finite strict unital Group-like V133() Subgroup of h

a |^ F is Element of the carrier of h

{(a |^ F)} is non zero V39() Element of K19( the carrier of h)

gr {(a |^ F)} is V60() finite strict unital Group-like V133() Subgroup of h

d is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

(F gcd G) * d is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

d * 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

b is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

(F gcd G) * b is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

(a |^ F) |^ d is Element of the carrier of h

b * (F gcd G) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

(b * (F gcd G)) * d is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

a |^ ((b * (F gcd G)) * d) is Element of the carrier of h

G * b is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

a |^ (G * b) is Element of the carrier of h

a |^ G is Element of the carrier of h

(a |^ G) |^ b is Element of the carrier of h

1_ h is non being_of_order_0 Element of the carrier of h

(1_ h) |^ b is Element of the carrier of h

ord (a |^ F) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

f is complex V32() integer ext-real set

f * F is complex V32() integer ext-real set

d is complex V32() integer ext-real set

d * G is complex V32() integer ext-real set

(f * F) + (d * G) is complex V32() integer ext-real set

b is Element of the carrier of h

i is complex V32() integer ext-real set

a |^ i is Element of the carrier of h

F * f is complex V32() integer ext-real set

G * d is complex V32() integer ext-real set

(F * f) + (G * d) is complex V32() integer ext-real set

((F * f) + (G * d)) * i is complex V32() integer ext-real set

(F * f) * i is complex V32() integer ext-real set

(G * d) * i is complex V32() integer ext-real set

((F * f) * i) + ((G * d) * i) is complex V32() integer ext-real set

f * i is complex V32() integer ext-real set

(a |^ F) |^ (f * i) is Element of the carrier of h

a |^ ((F * f) * i) is Element of the carrier of h

d * i is complex V32() integer ext-real set

G * (d * i) is complex V32() integer ext-real set

a |^ (G * (d * i)) is Element of the carrier of h

(a |^ ((F * f) * i)) * (a |^ (G * (d * i))) is Element of the carrier of h

the multF of h is Relation-like K20( the carrier of h, the carrier of h) -defined the carrier of h -valued Function-like quasi_total V22( the carrier of h) V39() Element of K19(K20(K20( the carrier of h, the carrier of h), the carrier of h))

K20( the carrier of h, the carrier of h) is V39() set

K20(K20( the carrier of h, the carrier of h), the carrier of h) is V39() set

K19(K20(K20( the carrier of h, the carrier of h), the carrier of h)) is V39() V43() set

K84( the carrier of h, the multF of h,(a |^ ((F * f) * i)),(a |^ (G * (d * i)))) is Element of the carrier of h

a |^ G is Element of the carrier of h

(a |^ G) |^ (d * i) is Element of the carrier of h

(a |^ ((F * f) * i)) * ((a |^ G) |^ (d * i)) is Element of the carrier of h

K84( the carrier of h, the multF of h,(a |^ ((F * f) * i)),((a |^ G) |^ (d * i))) is Element of the carrier of h

1_ h is non being_of_order_0 Element of the carrier of h

(1_ h) |^ (d * i) is Element of the carrier of h

(a |^ ((F * f) * i)) * ((1_ h) |^ (d * i)) is Element of the carrier of h

K84( the carrier of h, the multF of h,(a |^ ((F * f) * i)),((1_ h) |^ (d * i))) is Element of the carrier of h

(a |^ ((F * f) * i)) * (1_ h) is Element of the carrier of h

K84( the carrier of h, the multF of h,(a |^ ((F * f) * i)),(1_ h)) is Element of the carrier of h

F * (f * i) is complex V32() integer ext-real set

a |^ (F * (f * i)) is Element of the carrier of h

c

(a |^ F) |^ c

G is V60() unital Group-like V133() V135() cyclic multMagma

the carrier of G is non zero set

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total V22( the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is set

multMagma(# the carrier of G, the multF of G #) is strict unital Group-like V133() multMagma

F is V60() unital Group-like V133() V135() Subgroup of G

the carrier of F is non zero set

the multF of F is Relation-like K20( the carrier of F, the carrier of F) -defined the carrier of F -valued Function-like quasi_total V22( the carrier of F) Element of K19(K20(K20( the carrier of F, the carrier of F), the carrier of F))

K20( the carrier of F, the carrier of F) is set

K20(K20( the carrier of F, the carrier of F), the carrier of F) is set

K19(K20(K20( the carrier of F, the carrier of F), the carrier of F)) is set

multMagma(# the carrier of F, the multF of F #) is strict unital Group-like V133() multMagma

h is Element of the carrier of G

{h} is non zero V39() Element of K19( the carrier of G)

K19( the carrier of G) is set

gr {h} is V60() strict unital Group-like V133() V135() Subgroup of G

a is Element of the carrier of F

{a} is non zero V39() Element of K19( the carrier of F)

K19( the carrier of F) is set

gr {a} is V60() strict unital Group-like V133() V135() Subgroup of F

G is V60() unital Group-like V133() V135() cyclic multMagma

the carrier of G is non zero set

F is Element of the carrier of G

{F} is non zero V39() Element of K19( the carrier of G)

K19( the carrier of G) is set

gr {F} is V60() strict unital Group-like V133() V135() Subgroup of G

h is complex V32() integer ext-real set

a is complex V32() integer ext-real set

F |^ h is Element of the carrier of G

F |^ a is Element of the carrier of G

a - h is complex V32() integer ext-real set

h + 0 is complex V32() integer ext-real set

- h is complex V32() integer ext-real set

F |^ (- h) is Element of the carrier of G

(F |^ a) * (F |^ (- h)) is Element of the carrier of G

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total V22( the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is set

K84( the carrier of G, the multF of G,(F |^ a),(F |^ (- h))) is Element of the carrier of G

(F |^ h) " is Element of the carrier of G

(F |^ h) * ((F |^ h) ") is Element of the carrier of G

K84( the carrier of G, the multF of G,(F |^ h),((F |^ h) ")) is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

a + (- h) is complex V32() integer ext-real set

F |^ (a + (- h)) is Element of the carrier of G

b is complex V32() integer ext-real set

F |^ b is Element of the carrier of G

b mod (a - h) is complex V32() integer ext-real set

i is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F |^ i is Element of the carrier of G

b div (a - h) is complex V32() integer ext-real set

(b div (a - h)) * (a - h) is complex V32() integer ext-real set

((b div (a - h)) * (a - h)) + (b mod (a - h)) is complex V32() integer ext-real set

F |^ (((b div (a - h)) * (a - h)) + (b mod (a - h))) is Element of the carrier of G

(a - h) * (b div (a - h)) is complex V32() integer ext-real set

F |^ ((a - h) * (b div (a - h))) is Element of the carrier of G

F |^ (b mod (a - h)) is Element of the carrier of G

(F |^ ((a - h) * (b div (a - h)))) * (F |^ (b mod (a - h))) is Element of the carrier of G

K84( the carrier of G, the multF of G,(F |^ ((a - h) * (b div (a - h)))),(F |^ (b mod (a - h)))) is Element of the carrier of G

(1_ G) |^ (b div (a - h)) is Element of the carrier of G

((1_ G) |^ (b div (a - h))) * (F |^ (b mod (a - h))) is Element of the carrier of G

K84( the carrier of G, the multF of G,((1_ G) |^ (b div (a - h))),(F |^ (b mod (a - h)))) is Element of the carrier of G

(1_ G) * (F |^ (b mod (a - h))) is Element of the carrier of G

K84( the carrier of G, the multF of G,(1_ G),(F |^ (b mod (a - h)))) is Element of the carrier of G

d is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

b is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set

len b is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

dom b is V39() V154() V155() V156() V157() V158() V159() Element of K19(NAT)

Seg d is V39() d -element V154() V155() V156() V157() V158() V159() Element of K19(NAT)

rng b is V39() set

i is set

c

m is complex V32() integer ext-real set

F |^ m is Element of the carrier of G

m is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F |^ m is Element of the carrier of G

0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real positive non negative set

F |^ d is Element of the carrier of G

b . d is set

0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real positive non negative set

b . m is set

m is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

b . m is set

i is set

c

b . c

m is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F |^ m is Element of the carrier of G

i is set

c

F |^ c

b is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set

rng b is V39() set

h - a is complex V32() integer ext-real set

a + 0 is complex V32() integer ext-real set

- a is complex V32() integer ext-real set

F |^ (- a) is Element of the carrier of G

(F |^ h) * (F |^ (- a)) is Element of the carrier of G

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total V22( the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is set

K84( the carrier of G, the multF of G,(F |^ h),(F |^ (- a))) is Element of the carrier of G

(F |^ a) " is Element of the carrier of G

(F |^ a) * ((F |^ a) ") is Element of the carrier of G

K84( the carrier of G, the multF of G,(F |^ a),((F |^ a) ")) is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

h + (- a) is complex V32() integer ext-real set

F |^ (h + (- a)) is Element of the carrier of G

b is complex V32() integer ext-real set

F |^ b is Element of the carrier of G

b mod (h - a) is complex V32() integer ext-real set

i is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F |^ i is Element of the carrier of G

b div (h - a) is complex V32() integer ext-real set

(b div (h - a)) * (h - a) is complex V32() integer ext-real set

((b div (h - a)) * (h - a)) + (b mod (h - a)) is complex V32() integer ext-real set

F |^ (((b div (h - a)) * (h - a)) + (b mod (h - a))) is Element of the carrier of G

(h - a) * (b div (h - a)) is complex V32() integer ext-real set

F |^ ((h - a) * (b div (h - a))) is Element of the carrier of G

F |^ (b mod (h - a)) is Element of the carrier of G

(F |^ ((h - a) * (b div (h - a)))) * (F |^ (b mod (h - a))) is Element of the carrier of G

K84( the carrier of G, the multF of G,(F |^ ((h - a) * (b div (h - a)))),(F |^ (b mod (h - a)))) is Element of the carrier of G

(1_ G) |^ (b div (h - a)) is Element of the carrier of G

((1_ G) |^ (b div (h - a))) * (F |^ (b mod (h - a))) is Element of the carrier of G

K84( the carrier of G, the multF of G,((1_ G) |^ (b div (h - a))),(F |^ (b mod (h - a)))) is Element of the carrier of G

(1_ G) * (F |^ (b mod (h - a))) is Element of the carrier of G

K84( the carrier of G, the multF of G,(1_ G),(F |^ (b mod (h - a)))) is Element of the carrier of G

d is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

b is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set

len b is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

dom b is V39() V154() V155() V156() V157() V158() V159() Element of K19(NAT)

Seg d is V39() d -element V154() V155() V156() V157() V158() V159() Element of K19(NAT)

rng b is V39() set

i is set

c

m is complex V32() integer ext-real set

F |^ m is Element of the carrier of G

m is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F |^ m is Element of the carrier of G

0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real positive non negative set

F |^ d is Element of the carrier of G

b . d is set

0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real positive non negative set

b . m is set

m is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

b . m is set

i is set

c

b . c

m is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F |^ m is Element of the carrier of G

i is set

c

F |^ c

b is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set

rng b is V39() set

h is V60() finite unital Group-like V133() V135() cyclic multMagma

card h is 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

a is complex V32() integer ext-real set

F |^ a is Element of the carrier of G

1_ h is non being_of_order_0 Element of the carrier of h

the carrier of h is non zero V39() set

f is complex V32() integer ext-real set

F |^ f is Element of the carrier of G

h is complex V32() integer ext-real set

a is complex V32() integer ext-real set

F |^ h is Element of the carrier of G

F |^ a is Element of the carrier of G

f is complex V32() integer ext-real set

d is complex V32() integer ext-real set

F |^ f is Element of the carrier of G

F |^ d is Element of the carrier of G

G is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real positive non negative set

INT.Group G is V60() finite strict unital Group-like V133() V135() cyclic multMagma

Segm G is non zero V154() V155() V156() V157() V158() V159() Element of K19(omega)

K485(G) is Relation-like K20((Segm G),(Segm G)) -defined Segm G -valued Function-like quasi_total Element of K19(K20(K20((Segm G),(Segm G)),(Segm G)))

K20((Segm G),(Segm G)) is set

K20(K20((Segm G),(Segm G)),(Segm G)) is set

K19(K20(K20((Segm G),(Segm G)),(Segm G))) is set

multMagma(# (Segm G),K485(G) #) is strict multMagma

the carrier of (INT.Group G) is non zero V39() set

F is Element of the carrier of (INT.Group G)

G is V60() finite strict unital Group-like V133() V135() cyclic multMagma

card G is 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

INT.Group (card G) is V60() finite strict unital Group-like V133() V135() cyclic multMagma

Segm (card G) is non zero V154() V155() V156() V157() V158() V159() Element of K19(omega)

K485((card G)) is Relation-like K20((Segm (card G)),(Segm (card G))) -defined Segm (card G) -valued Function-like quasi_total Element of K19(K20(K20((Segm (card G)),(Segm (card G))),(Segm (card G))))

K20((Segm (card G)),(Segm (card G))) is set

K20(K20((Segm (card G)),(Segm (card G))),(Segm (card G))) is set

K19(K20(K20((Segm (card G)),(Segm (card G))),(Segm (card G)))) is set

multMagma(# (Segm (card G)),K485((card G)) #) is strict multMagma

the carrier of G is non zero V39() set

h is Element of the carrier of G

a is Element of the carrier of G

f is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

h |^ f is Element of the carrier of G

d is complex V32() integer ext-real set

h |^ d is Element of the carrier of G

{h} is non zero V39() Element of K19( the carrier of G)

K19( the carrier of G) is V39() V43() set

gr {h} is V60() finite strict unital Group-like V133() V135() Subgroup of G

the carrier of (INT.Group (card G)) is non zero V39() set

K20( the carrier of (INT.Group (card G)), the carrier of G) is V39() set

K19(K20( the carrier of (INT.Group (card G)), the carrier of G)) is V39() V43() set

a is Relation-like the carrier of (INT.Group (card G)) -defined the carrier of G -valued Function-like quasi_total V39() Element of K19(K20( the carrier of (INT.Group (card G)), the carrier of G))

f is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative Element of the carrier of (INT.Group (card G))

d is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative Element of the carrier of (INT.Group (card G))

f * d is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative Element of the carrier of (INT.Group (card G))

the multF of (INT.Group (card G)) is Relation-like K20( the carrier of (INT.Group (card G)), the carrier of (INT.Group (card G))) -defined the carrier of (INT.Group (card G)) -valued Function-like quasi_total V22( the carrier of (INT.Group (card G))) V39() Element of K19(K20(K20( the carrier of (INT.Group (card G)), the carrier of (INT.Group (card G))), the carrier of (INT.Group (card G))))

K20( the carrier of (INT.Group (card G)), the carrier of (INT.Group (card G))) is V39() set

K20(K20( the carrier of (INT.Group (card G)), the carrier of (INT.Group (card G))), the carrier of (INT.Group (card G))) is V39() set

K19(K20(K20( the carrier of (INT.Group (card G)), the carrier of (INT.Group (card G))), the carrier of (INT.Group (card G)))) is V39() V43() set

K84( the carrier of (INT.Group (card G)), the multF of (INT.Group (card G)),f,d) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative Element of the carrier of (INT.Group (card G))

a . (f * d) is Element of the carrier of G

a . f is Element of the carrier of G

a . d is Element of the carrier of G

(a . f) * (a . d) is Element of the carrier of G

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total V22( the carrier of G) V39() Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is V39() set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is V39() set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is V39() V43() set

K84( the carrier of G, the multF of G,(a . f),(a . d)) is Element of the carrier of G

f + d is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

(f + d) mod (card G) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

(f + d) div (card G) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

(card G) * ((f + d) div (card G)) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

(f + d) - ((card G) * ((f + d) div (card G))) is complex V32() integer ext-real set

- ((card G) * ((f + d) div (card G))) is complex V32() integer ext-real non positive set

(f + d) + (- ((card G) * ((f + d) div (card G)))) is complex V32() integer ext-real set

h |^ ((f + d) + (- ((card G) * ((f + d) div (card G))))) is Element of the carrier of G

h |^ (f + d) is Element of the carrier of G

h |^ (- ((card G) * ((f + d) div (card G)))) is Element of the carrier of G

(h |^ (f + d)) * (h |^ (- ((card G) * ((f + d) div (card G))))) is Element of the carrier of G

K84( the carrier of G, the multF of G,(h |^ (f + d)),(h |^ (- ((card G) * ((f + d) div (card G)))))) is Element of the carrier of G

h |^ ((card G) * ((f + d) div (card G))) is Element of the carrier of G

(h |^ ((card G) * ((f + d) div (card G)))) " is Element of the carrier of G

(h |^ (f + d)) * ((h |^ ((card G) * ((f + d) div (card G)))) ") is Element of the carrier of G

K84( the carrier of G, the multF of G,(h |^ (f + d)),((h |^ ((card G) * ((f + d) div (card G)))) ")) is Element of the carrier of G

h |^ (card G) is Element of the carrier of G

(h |^ (card G)) |^ ((f + d) div (card G)) is Element of the carrier of G

((h |^ (card G)) |^ ((f + d) div (card G))) " is Element of the carrier of G

(h |^ (f + d)) * (((h |^ (card G)) |^ ((f + d) div (card G))) ") is Element of the carrier of G

K84( the carrier of G, the multF of G,(h |^ (f + d)),(((h |^ (card G)) |^ ((f + d) div (card G))) ")) is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

(1_ G) |^ ((f + d) div (card G)) is Element of the carrier of G

((1_ G) |^ ((f + d) div (card G))) " is Element of the carrier of G

(h |^ (f + d)) * (((1_ G) |^ ((f + d) div (card G))) ") is Element of the carrier of G

K84( the carrier of G, the multF of G,(h |^ (f + d)),(((1_ G) |^ ((f + d) div (card G))) ")) is Element of the carrier of G

(1_ G) " is Element of the carrier of G

(h |^ (f + d)) * ((1_ G) ") is Element of the carrier of G

K84( the carrier of G, the multF of G,(h |^ (f + d)),((1_ G) ")) is Element of the carrier of G

(h |^ (f + d)) * (1_ G) is Element of the carrier of G

K84( the carrier of G, the multF of G,(h |^ (f + d)),(1_ G)) is Element of the carrier of G

h |^ f is Element of the carrier of G

h |^ d is Element of the carrier of G

(h |^ f) * (h |^ d) is Element of the carrier of G

K84( the carrier of G, the multF of G,(h |^ f),(h |^ d)) is Element of the carrier of G

(a . f) * (h |^ d) is Element of the carrier of G

K84( the carrier of G, the multF of G,(a . f),(h |^ d)) is Element of the carrier of G

f is set

dom a is V39() set

a . f is set

d is set

a . d is set

i is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative Element of the carrier of (INT.Group (card G))

h |^ i is Element of the carrier of G

b is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative Element of the carrier of (INT.Group (card G))

a . b is Element of the carrier of G

h |^ b is Element of the carrier of G

c

m is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

1_ G is non being_of_order_0 Element of the carrier of G

m1 is complex V32() integer ext-real set

p1 is complex V32() integer ext-real set

m1 - p1 is complex V32() integer ext-real set

r1 is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

n1 is complex V32() integer ext-real set

n1 + 0 is complex V32() integer ext-real set

- p1 is complex V32() integer ext-real set

m1 + (- p1) is complex V32() integer ext-real set

h |^ m1 is Element of the carrier of G

- p1 is complex V32() integer ext-real set

h |^ (- p1) is Element of the carrier of G

(h |^ m1) * (h |^ (- p1)) is Element of the carrier of G

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total V22( the carrier of G) V39() Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is V39() set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is V39() set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is V39() V43() set

K84( the carrier of G, the multF of G,(h |^ m1),(h |^ (- p1))) is Element of the carrier of G

p1 + (- p1) is complex V32() integer ext-real set

h |^ (p1 + (- p1)) is Element of the carrier of G

m1 + (- p1) is complex V32() integer ext-real set

h |^ (m1 + (- p1)) is Element of the carrier of G

h |^ 0 is Element of the carrier of G

r1 is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

r1 is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

p1 is complex V32() integer ext-real set

m1 is complex V32() integer ext-real set

p1 - m1 is complex V32() integer ext-real set

r1 is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

n1 is complex V32() integer ext-real set

n1 + 0 is complex V32() integer ext-real set

- m1 is complex V32() integer ext-real set

p1 + (- m1) is complex V32() integer ext-real set

h |^ p1 is Element of the carrier of G

- m1 is complex V32() integer ext-real set

h |^ (- m1) is Element of the carrier of G

(h |^ p1) * (h |^ (- m1)) is Element of the carrier of G

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total V22( the carrier of G) V39() Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is V39() set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is V39() set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is V39() V43() set

K84( the carrier of G, the multF of G,(h |^ p1),(h |^ (- m1))) is Element of the carrier of G

m1 + (- m1) is complex V32() integer ext-real set

h |^ (m1 + (- m1)) is Element of the carrier of G

p1 + (- m1) is complex V32() integer ext-real set

h |^ (p1 + (- m1)) is Element of the carrier of G

h |^ 0 is Element of the carrier of G

r1 is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

r1 is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

ord h is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

m1 is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

h |^ m1 is Element of the carrier of G

dom a is V39() set

rng a is V39() set

f is set

d is Element of the carrier of G

b is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

h |^ b is Element of the carrier of G

b mod (card G) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

b div (card G) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

(card G) * (b div (card G)) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

((card G) * (b div (card G))) + (b mod (card G)) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

h |^ (((card G) * (b div (card G))) + (b mod (card G))) is Element of the carrier of G

h |^ ((card G) * (b div (card G))) is Element of the carrier of G

h |^ (b mod (card G)) is Element of the carrier of G

(h |^ ((card G) * (b div (card G)))) * (h |^ (b mod (card G))) is Element of the carrier of G

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total V22( the carrier of G) V39() Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is V39() set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is V39() set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is V39() V43() set

K84( the carrier of G, the multF of G,(h |^ ((card G) * (b div (card G)))),(h |^ (b mod (card G)))) is Element of the carrier of G

h |^ (card G) is Element of the carrier of G

(h |^ (card G)) |^ (b div (card G)) is Element of the carrier of G

((h |^ (card G)) |^ (b div (card G))) * (h |^ (b mod (card G))) is Element of the carrier of G

K84( the carrier of G, the multF of G,((h |^ (card G)) |^ (b div (card G))),(h |^ (b mod (card G)))) is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

(1_ G) |^ (b div (card G)) is Element of the carrier of G

((1_ G) |^ (b div (card G))) * (h |^ (b mod (card G))) is Element of the carrier of G

K84( the carrier of G, the multF of G,((1_ G) |^ (b div (card G))),(h |^ (b mod (card G)))) is Element of the carrier of G

(1_ G) * (h |^ (b mod (card G))) is Element of the carrier of G

K84( the carrier of G, the multF of G,(1_ G),(h |^ (b mod (card G)))) is Element of the carrier of G

c

a . c

f is Relation-like the carrier of (INT.Group (card G)) -defined the carrier of G -valued Function-like quasi_total V39() V140( INT.Group (card G),G) Element of K19(K20( the carrier of (INT.Group (card G)), the carrier of G))

a is Relation-like the carrier of (INT.Group (card G)) -defined the carrier of G -valued Function-like quasi_total V39() V140( INT.Group (card G),G) Element of K19(K20( the carrier of (INT.Group (card G)), the carrier of G))

G is V60() strict unital Group-like V133() V135() cyclic multMagma

the carrier of G is non zero set

F is Element of the carrier of G

K20( the carrier of INT.Group, the carrier of G) is set

K19(K20( the carrier of INT.Group, the carrier of G)) is set

h is Relation-like the carrier of INT.Group -defined the carrier of G -valued Function-like quasi_total Element of K19(K20( the carrier of INT.Group, the carrier of G))

{F} is non zero V39() Element of K19( the carrier of G)

K19( the carrier of G) is set

gr {F} is V60() strict unital Group-like V133() V135() Subgroup of G

a is set

dom h is set

h . a is set

f is set

h . f is set

b is complex V32() integer V35() ext-real Element of the carrier of INT.Group

@' b is complex V32() integer V35() ext-real Element of the carrier of INT.Group

F |^ (@' b) is Element of the carrier of G

d is complex V32() integer V35() ext-real Element of the carrier of INT.Group

h . d is Element of the carrier of G

@' d is complex V32() integer V35() ext-real Element of the carrier of INT.Group

F |^ (@' d) is Element of the carrier of G

dom h is set

rng h is set

a is set

f is Element of the carrier of G

d is complex V32() integer ext-real set

F |^ d is Element of the carrier of G

b is complex V32() integer V35() ext-real Element of the carrier of INT.Group

@' b is complex V32() integer V35() ext-real Element of the carrier of INT.Group

h . b is Element of the carrier of G

a is complex V32() integer V35() ext-real Element of the carrier of INT.Group

h . a is Element of the carrier of G

f is complex V32() integer V35() ext-real Element of the carrier of INT.Group

a * f is complex V32() integer V35() ext-real Element of the carrier of INT.Group

the multF of INT.Group is Relation-like K20( the carrier of INT.Group, the carrier of INT.Group) -defined the carrier of INT.Group -valued Function-like quasi_total V22( the carrier of INT.Group) Element of K19(K20(K20( the carrier of INT.Group, the carrier of INT.Group), the carrier of INT.Group))

K20( the carrier of INT.Group, the carrier of INT.Group) is set

K20(K20( the carrier of INT.Group, the carrier of INT.Group), the carrier of INT.Group) is set

K19(K20(K20( the carrier of INT.Group, the carrier of INT.Group), the carrier of INT.Group)) is set

K84( the carrier of INT.Group, the multF of INT.Group,a,f) is complex V32() integer V35() ext-real Element of the carrier of INT.Group

K198(a,f) is complex V32() integer V35() ext-real Element of INT

h . (a * f) is Element of the carrier of G

h . f is Element of the carrier of G

(h . a) * (h . f) is Element of the carrier of G

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total V22( the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is set

K84( the carrier of G, the multF of G,(h . a),(h . f)) is Element of the carrier of G

@' (a * f) is complex V32() integer V35() ext-real Element of the carrier of INT.Group

@' a is complex V32() integer V35() ext-real Element of the carrier of INT.Group

@' f is complex V32() integer V35() ext-real Element of the carrier of INT.Group

(@' a) + (@' f) is complex V32() integer ext-real set

F |^ ((@' a) + (@' f)) is Element of the carrier of G

F |^ (@' a) is Element of the carrier of G

F |^ (@' f) is Element of the carrier of G

(F |^ (@' a)) * (F |^ (@' f)) is Element of the carrier of G

K84( the carrier of G, the multF of G,(F |^ (@' a)),(F |^ (@' f))) is Element of the carrier of G

(h . a) * (F |^ (@' f)) is Element of the carrier of G

K84( the carrier of G, the multF of G,(h . a),(F |^ (@' f))) is Element of the carrier of G

a is Relation-like the carrier of INT.Group -defined the carrier of G -valued Function-like quasi_total V140( INT.Group ,G) Element of K19(K20( the carrier of INT.Group, the carrier of G))

h is Relation-like the carrier of INT.Group -defined the carrier of G -valued Function-like quasi_total V140( INT.Group ,G) Element of K19(K20( the carrier of INT.Group, the carrier of G))

F is V60() finite strict unital Group-like V133() V135() cyclic multMagma

card F is 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

G is V60() finite strict unital Group-like V133() V135() cyclic multMagma

card G is 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

INT.Group (card F) is V60() finite strict unital Group-like V133() V135() cyclic multMagma

Segm (card F) is non zero V154() V155() V156() V157() V158() V159() Element of K19(omega)

K485((card F)) is Relation-like K20((Segm (card F)),(Segm (card F))) -defined Segm (card F) -valued Function-like quasi_total Element of K19(K20(K20((Segm (card F)),(Segm (card F))),(Segm (card F))))

K20((Segm (card F)),(Segm (card F))) is set

K20(K20((Segm (card F)),(Segm (card F))),(Segm (card F))) is set

K19(K20(K20((Segm (card F)),(Segm (card F))),(Segm (card F)))) is set

multMagma(# (Segm (card F)),K485((card F)) #) is strict multMagma

G is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F is V60() finite strict unital Group-like V133() multMagma

card F is 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

h is V60() finite strict unital Group-like V133() multMagma

card h is 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

G is V60() finite strict unital Group-like V133() multMagma

card G is 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

F is V60() finite strict unital Group-like V133() multMagma

card F is 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

G is V60() finite strict unital Group-like V133() multMagma

card G is 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

F is V60() finite strict unital Group-like V133() Subgroup of G

(1). G is V60() finite strict unital Group-like V133() V135() cyclic Subgroup of G

G is V60() finite strict unital Group-like V133() multMagma

card G is 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

G is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

F is V60() finite strict unital Group-like V133() multMagma

card F is 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

h is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

a is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

h * a is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

the carrier of F is non zero V39() set

f is Element of the carrier of F

{f} is non zero V39() Element of K19( the carrier of F)

K19( the carrier of F) is V39() V43() set

gr {f} is V60() finite strict unital Group-like V133() Subgroup of F

f |^ a is Element of the carrier of F

{(f |^ a)} is non zero V39() Element of K19( the carrier of F)

gr {(f |^ a)} is V60() finite strict unital Group-like V133() Subgroup of F

card (gr {(f |^ a)}) is 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

ord (f |^ a) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

d is V60() finite strict unital Group-like V133() Subgroup of F

card d is 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

b is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

f |^ b is Element of the carrier of F

{(f |^ b)} is non zero V39() Element of K19( the carrier of F)

gr {(f |^ b)} is V60() finite strict unital Group-like V133() Subgroup of F

b * h is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

i is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

G * i is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

a * i is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

c

1 / c

(1 / c

((1 / c

c

(c

(1 / c

1 * b is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

c

(c

((c

1 * a is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

(1 * a) * i is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

c

a * c

d is V60() finite strict unital Group-like V133() Subgroup of F

card d is 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

a is V60() finite strict unital Group-like V133() Subgroup of F

card a is 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

G is V60() unital Group-like V133() V135() cyclic multMagma

the carrier of G is non zero set

F is Element of the carrier of G

{F} is non zero V39() Element of K19( the carrier of G)

K19( the carrier of G) is set

gr {F} is V60() strict unital Group-like V133() V135() Subgroup of G

h is V60() unital Group-like V133() multMagma

the carrier of h is non zero set

K20( the carrier of h, the carrier of G) is set

K19(K20( the carrier of h, the carrier of G)) is set

a is Relation-like the carrier of h -defined the carrier of G -valued Function-like quasi_total V140(h,G) Element of K19(K20( the carrier of h, the carrier of G))

Image a is V60() strict unital Group-like V133() V135() Subgroup of G

G is V60() finite strict unital Group-like V133() V135() cyclic multMagma

card G is 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

the carrier of G is non zero V39() set

h is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

2 * h is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

a is Element of the carrier of G

{a} is non zero V39() Element of K19( the carrier of G)

K19( the carrier of G) is V39() V43() set

gr {a} is V60() finite strict unital Group-like V133() V135() Subgroup of G

ord a is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

a |^ h is Element of the carrier of G

ord (a |^ h) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

(a |^ h) |^ 2 is Element of the carrier of G

a |^ (card G) is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

f is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

(a |^ h) |^ f is Element of the carrier of G

h * f is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

a |^ (h * f) is Element of the carrier of G

f is Element of the carrier of G

ord f is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

d is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

a |^ d is Element of the carrier of G

b is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

h * b is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

i is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

(h * b) + i is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

2 * i is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

b div 2 is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT

2 * (b div 2) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set

b mod 2 is epsilon-transitive epsilon-connected ordinal natural