:: 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₉ is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
(G * i) + c₉ is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
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₉ is Element of the carrier of a
(d |^ (G * i)) * (d |^ c₉) is Element of the carrier of a
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₉)) is Element of the carrier of a
d |^ G is Element of the carrier of a
(d |^ G) |^ i is Element of the carrier of a
((d |^ G) |^ i) * (d |^ c₉) is Element of the carrier of a
K84( the carrier of a, the multF of a,((d |^ G) |^ i),(d |^ c₉)) is Element of the carrier of a
(1_ a) |^ i is Element of the carrier of a
((1_ a) |^ i) * (d |^ c₉) is Element of the carrier of a
K84( the carrier of a, the multF of a,((1_ a) |^ i),(d |^ c₉)) is Element of the carrier of a
(1_ a) * (d |^ c₉) is Element of the carrier of a
K84( the carrier of a, the multF of a,(1_ a),(d |^ c₉)) is Element of the carrier of a
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₉ is complex V32() integer ext-real set
(a |^ F) |^ c₉ is Element of the carrier of h
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₉ is Element of the carrier of G
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₉ is set
b . c₉ 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
F |^ m is Element of the carrier of G
i is set
c₉ 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 |^ c₉ is Element of the carrier of G
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₉ is Element of the carrier of G
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₉ is set
b . c₉ 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
F |^ m is Element of the carrier of G
i is set
c₉ 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 |^ c₉ is Element of the carrier of G
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₉ is epsilon-transitive epsilon-connected ordinal natural complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT
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₉ is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative Element of the carrier of (INT.Group (card G))
a . c₉ is Element of the carrier of G
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₉ is complex V32() integer ext-real set
1 / c₉ is complex V32() ext-real set
(1 / c₉) * c₉ is complex V32() ext-real set
((1 / c₉) * c₉) * b is complex V32() ext-real set
c₉ * a is complex V32() integer ext-real set
(c₉ * a) * i is complex V32() integer ext-real set
(1 / c₉) * ((c₉ * a) * i) is complex V32() ext-real set
1 * b is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
c₉ * (1 / c₉) is complex V32() ext-real set
(c₉ * (1 / c₉)) * a is complex V32() ext-real set
((c₉ * (1 / c₉)) * a) * i is complex V32() ext-real set
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₉ is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
a * c₉ is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
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 complex V32() integer V35() ext-real non negative V154() V155() V156() V157() V158() V159() Element of NAT
(2 * (b div 2)) + (b mod 2) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
h * ((2 * (b div 2)) + (b mod 2)) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
a |^ (h * ((2 * (b div 2)) + (b mod 2))) is Element of the carrier of G
h * 2 is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
(h * 2) * (b div 2) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
h * (b mod 2) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
((h * 2) * (b div 2)) + (h * (b mod 2)) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
a |^ (((h * 2) * (b div 2)) + (h * (b mod 2))) is Element of the carrier of G
a |^ ((h * 2) * (b div 2)) is Element of the carrier of G
a |^ (h * (b mod 2)) is Element of the carrier of G
(a |^ ((h * 2) * (b div 2))) * (a |^ (h * (b mod 2))) 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 |^ ((h * 2) * (b div 2))),(a |^ (h * (b mod 2)))) is Element of the carrier of G
a |^ (h * 2) is Element of the carrier of G
(a |^ (h * 2)) |^ (b div 2) is Element of the carrier of G
((a |^ (h * 2)) |^ (b div 2)) * (a |^ (h * (b mod 2))) is Element of the carrier of G
K84( the carrier of G, the multF of G,((a |^ (h * 2)) |^ (b div 2)),(a |^ (h * (b mod 2)))) is Element of the carrier of G
(1_ G) |^ (b div 2) is Element of the carrier of G
((1_ G) |^ (b div 2)) * (a |^ (h * (b mod 2))) is Element of the carrier of G
K84( the carrier of G, the multF of G,((1_ G) |^ (b div 2)),(a |^ (h * (b mod 2)))) is Element of the carrier of G
(1_ G) * (a |^ (h * (b mod 2))) is Element of the carrier of G
K84( the carrier of G, the multF of G,(1_ G),(a |^ (h * (b mod 2)))) is Element of the carrier of G
(a |^ d) |^ 2 is Element of the carrier of G
((h * b) + i) * 2 is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
a |^ (((h * b) + i) * 2) is Element of the carrier of G
(card G) * b is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
i * 2 is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
((card G) * b) + (i * 2) is epsilon-transitive epsilon-connected ordinal natural complex V32() integer ext-real non negative set
a |^ (((card G) * b) + (i * 2)) is Element of the carrier of G
a |^ ((card G) * b) is Element of the carrier of G
a |^ (i * 2) is Element of the carrier of G
(a |^ ((card G) * b)) * (a |^ (i * 2)) 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 |^ ((card G) * b)),(a |^ (i * 2))) is Element of the carrier of G
a |^ (ord a) is Element of the carrier of G
(a |^ (ord a)) |^ b is Element of the carrier of G
((a |^ (ord a)) |^ b) * (a |^ (i * 2)) is Element of the carrier of G
K84( the carrier of G, the multF of G,((a |^ (ord a)) |^ b),(a |^ (i * 2))) is Element of the carrier of G
(1_ G) |^ b is Element of the carrier of G
((1_ G) |^ b) * (a |^ (i * 2)) is Element of the carrier of G
K84( the carrier of G, the multF of G,((1_ G) |^ b),(a |^ (i * 2))) is Element of the carrier of G
(1_ G) * (a |^ (i * 2)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(1_ G),(a |^ (i * 2))) is Element of the carrier of G
a |^ (2 * i) is Element of the carrier of G
G is V60() unital Group-like V133() multMagma
center G is V60() strict unital Group-like V133() 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
h is Element of the carrier of G
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
{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
card (gr {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() unital Group-like V133() multMagma
the carrier of G is non zero set
F is V60() strict unital Group-like V133() multMagma
the carrier of F is non zero set
K20( the carrier of F, the carrier of G) is set
K19(K20( the carrier of F, the carrier of G)) is set
h is Relation-like the carrier of F -defined the carrier of G -valued Function-like quasi_total V140(F,G) Element of K19(K20( the carrier of F, the carrier of G))
Image 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
the carrier of (Image h) is non zero set
h . a is Element of the carrier of G
f is Element of the carrier of (Image h)
{f} is non zero V39() Element of K19( the carrier of (Image h))
K19( the carrier of (Image h)) is set
gr {f} is V60() strict unital Group-like V133() Subgroup of Image h
d is Element of the carrier of (Image h)
b is Element of the carrier of F
h . b is Element of the carrier of G
i is complex V32() integer ext-real set
a |^ i is Element of the carrier of F
f |^ i is Element of the carrier of (Image h)
(h . a) |^ i is Element of the carrier of G
f is Element of the carrier of (Image h)
{f} is non zero V39() Element of K19( the carrier of (Image h))
K19( the carrier of (Image h)) is set
gr {f} is V60() strict unital Group-like V133() Subgroup of Image h
G is V60() strict unital Group-like V133() multMagma
F is V60() strict unital Group-like V133() multMagma
the carrier of G is non zero set
the carrier of F is non zero set
K20( the carrier of G, the carrier of F) is set
K19(K20( the carrier of G, the carrier of F)) is set
h is Relation-like the carrier of G -defined the carrier of F -valued Function-like quasi_total V140(G,F) Element of K19(K20( the carrier of G, the carrier of F))
Image h is V60() strict unital Group-like V133() Subgroup of F