REAL is non empty V37() set
NAT is non empty V24() V25() V26() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V37() set
RAT is non empty V37() set
INT is non empty V37() set
[:COMPLEX,COMPLEX:] is non empty set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is non empty set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty set
[:[:NAT,NAT:],NAT:] is non empty set
bool [:[:NAT,NAT:],NAT:] is non empty set
NAT is non empty V24() V25() V26() set
bool NAT is non empty set
bool NAT is non empty set
K243() is set
1 is non empty V24() V25() V26() V30() V31() V32() V33() ext-real positive non negative Element of NAT
K502() is non empty strict unital Group-like associative commutative cyclic multMagma
the carrier of K502() is non empty V171() set
{} is functional empty V24() V25() V26() V28() V29() V30() V31() V32() V33() FinSequence-membered ext-real non positive non negative set
2 is non empty V24() V25() V26() V30() V31() V32() V33() ext-real positive non negative Element of NAT
3 is non empty V24() V25() V26() V30() V31() V32() V33() ext-real positive non negative Element of NAT
Seg 1 is non empty V37() V44(1) Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V32() V33() ext-real Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty set
Seg 2 is non empty V37() V44(2) Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V32() V33() ext-real Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty set
0 is functional empty V24() V25() V26() V28() V29() V30() V31() V32() V33() FinSequence-membered ext-real non positive non negative Element of NAT
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
F is Element of the carrier of G
R is Element of the carrier of G
F |^ R is Element of the carrier of G
R " is Element of the carrier of G
(R ") * F is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) V22( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
K84( the carrier of G, the multF of G,(R "),F) is Element of the carrier of G
((R ") * F) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * F),R) is Element of the carrier of G
[.F,R.] is Element of the carrier of G
F " is Element of the carrier of G
(F ") * (R ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(F "),(R ")) is Element of the carrier of G
((F ") * (R ")) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * (R ")),F) is Element of the carrier of G
(((F ") * (R ")) * F) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,(((F ") * (R ")) * F),R) is Element of the carrier of G
F * [.F,R.] is Element of the carrier of G
K84( the carrier of G, the multF of G,F,[.F,R.]) is Element of the carrier of G
F * R is Element of the carrier of G
K84( the carrier of G, the multF of G,F,R) is Element of the carrier of G
((F ") * (R ")) * (F * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * (R ")),(F * R)) is Element of the carrier of G
F * (((F ") * (R ")) * (F * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,F,(((F ") * (R ")) * (F * R))) is Element of the carrier of G
(R ") * (F * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),(F * R)) is Element of the carrier of G
(F ") * ((R ") * (F * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(F "),((R ") * (F * R))) is Element of the carrier of G
F * ((F ") * ((R ") * (F * R))) is Element of the carrier of G
K84( the carrier of G, the multF of G,F,((F ") * ((R ") * (F * R)))) is Element of the carrier of G
F * (F ") is Element of the carrier of G
K84( the carrier of G, the multF of G,F,(F ")) is Element of the carrier of G
(F * (F ")) * ((R ") * (F * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(F * (F ")),((R ") * (F * R))) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * ((R ") * (F * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(1_ G),((R ") * (F * R))) is Element of the carrier of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
F is Element of the carrier of G
R is Element of the carrier of G
[.F,R.] is Element of the carrier of G
F " is Element of the carrier of G
R " is Element of the carrier of G
(F ") * (R ") is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) V22( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
K84( the carrier of G, the multF of G,(F "),(R ")) is Element of the carrier of G
((F ") * (R ")) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * (R ")),F) is Element of the carrier of G
(((F ") * (R ")) * F) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,(((F ") * (R ")) * F),R) is Element of the carrier of G
[.F,R.] " is Element of the carrier of G
[.F,(R ").] is Element of the carrier of G
(R ") " is Element of the carrier of G
(F ") * ((R ") ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(F "),((R ") ")) is Element of the carrier of G
((F ") * ((R ") ")) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * ((R ") ")),F) is Element of the carrier of G
(((F ") * ((R ") ")) * F) * (R ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(((F ") * ((R ") ")) * F),(R ")) is Element of the carrier of G
[.F,(R ").] |^ R is Element of the carrier of G
(R ") * [.F,(R ").] is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),[.F,(R ").]) is Element of the carrier of G
((R ") * [.F,(R ").]) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * [.F,(R ").]),R) is Element of the carrier of G
F * R is Element of the carrier of G
K84( the carrier of G, the multF of G,F,R) is Element of the carrier of G
((F ") * (R ")) * (F * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * (R ")),(F * R)) is Element of the carrier of G
(((F ") * (R ")) * (F * R)) " is Element of the carrier of G
(F * R) " is Element of the carrier of G
((F ") * (R ")) " is Element of the carrier of G
((F * R) ") * (((F ") * (R ")) ") is Element of the carrier of G
K84( the carrier of G, the multF of G,((F * R) "),(((F ") * (R ")) ")) is Element of the carrier of G
(R ") * (F ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),(F ")) is Element of the carrier of G
((R ") * (F ")) * (((F ") * (R ")) ") is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (F ")),(((F ") * (R ")) ")) is Element of the carrier of G
(F ") " is Element of the carrier of G
((R ") ") * ((F ") ") is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") "),((F ") ")) is Element of the carrier of G
((R ") * (F ")) * (((R ") ") * ((F ") ")) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (F ")),(((R ") ") * ((F ") "))) is Element of the carrier of G
R * F is Element of the carrier of G
K84( the carrier of G, the multF of G,R,F) is Element of the carrier of G
(F ") * (R * F) is Element of the carrier of G
K84( the carrier of G, the multF of G,(F "),(R * F)) is Element of the carrier of G
(R ") * ((F ") * (R * F)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),((F ") * (R * F))) is Element of the carrier of G
(F ") * R is Element of the carrier of G
K84( the carrier of G, the multF of G,(F "),R) is Element of the carrier of G
((F ") * R) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * R),F) is Element of the carrier of G
(R ") * (((F ") * R) * F) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),(((F ") * R) * F)) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
((R ") * (((F ") * R) * F)) * (1_ G) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (((F ") * R) * F)),(1_ G)) is Element of the carrier of G
(R ") * R is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),R) is Element of the carrier of G
((R ") * (((F ") * R) * F)) * ((R ") * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (((F ") * R) * F)),((R ") * R)) is Element of the carrier of G
((R ") * (((F ") * R) * F)) * (R ") is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (((F ") * R) * F)),(R ")) is Element of the carrier of G
(((R ") * (((F ") * R) * F)) * (R ")) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,(((R ") * (((F ") * R) * F)) * (R ")),R) is Element of the carrier of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
F is Element of the carrier of G
F " is Element of the carrier of G
R is Element of the carrier of G
[.F,R.] is Element of the carrier of G
R " is Element of the carrier of G
(F ") * (R ") is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) V22( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
K84( the carrier of G, the multF of G,(F "),(R ")) is Element of the carrier of G
((F ") * (R ")) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * (R ")),F) is Element of the carrier of G
(((F ") * (R ")) * F) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,(((F ") * (R ")) * F),R) is Element of the carrier of G
[.F,R.] " is Element of the carrier of G
[.(F "),R.] is Element of the carrier of G
(F ") " is Element of the carrier of G
((F ") ") * (R ") is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") "),(R ")) is Element of the carrier of G
(((F ") ") * (R ")) * (F ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(((F ") ") * (R ")),(F ")) is Element of the carrier of G
((((F ") ") * (R ")) * (F ")) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((((F ") ") * (R ")) * (F ")),R) is Element of the carrier of G
[.(F "),R.] |^ F is Element of the carrier of G
(F ") * [.(F "),R.] is Element of the carrier of G
K84( the carrier of G, the multF of G,(F "),[.(F "),R.]) is Element of the carrier of G
((F ") * [.(F "),R.]) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * [.(F "),R.]),F) is Element of the carrier of G
F * R is Element of the carrier of G
K84( the carrier of G, the multF of G,F,R) is Element of the carrier of G
((F ") * (R ")) * (F * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * (R ")),(F * R)) is Element of the carrier of G
(((F ") * (R ")) * (F * R)) " is Element of the carrier of G
(F * R) " is Element of the carrier of G
((F ") * (R ")) " is Element of the carrier of G
((F * R) ") * (((F ") * (R ")) ") is Element of the carrier of G
K84( the carrier of G, the multF of G,((F * R) "),(((F ") * (R ")) ")) is Element of the carrier of G
(R ") * (F ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),(F ")) is Element of the carrier of G
((R ") * (F ")) * (((F ") * (R ")) ") is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (F ")),(((F ") * (R ")) ")) is Element of the carrier of G
(R ") " is Element of the carrier of G
((R ") ") * ((F ") ") is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") "),((F ") ")) is Element of the carrier of G
((R ") * (F ")) * (((R ") ") * ((F ") ")) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (F ")),(((R ") ") * ((F ") "))) is Element of the carrier of G
R * F is Element of the carrier of G
K84( the carrier of G, the multF of G,R,F) is Element of the carrier of G
(F ") * (R * F) is Element of the carrier of G
K84( the carrier of G, the multF of G,(F "),(R * F)) is Element of the carrier of G
(R ") * ((F ") * (R * F)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),((F ") * (R * F))) is Element of the carrier of G
(F ") * R is Element of the carrier of G
K84( the carrier of G, the multF of G,(F "),R) is Element of the carrier of G
((F ") * R) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * R),F) is Element of the carrier of G
(R ") * (((F ") * R) * F) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),(((F ") * R) * F)) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * ((R ") * (((F ") * R) * F)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(1_ G),((R ") * (((F ") * R) * F))) is Element of the carrier of G
(F ") * F is Element of the carrier of G
K84( the carrier of G, the multF of G,(F "),F) is Element of the carrier of G
((F ") * F) * ((R ") * (((F ") * R) * F)) is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * F),((R ") * (((F ") * R) * F))) is Element of the carrier of G
F * ((R ") * (((F ") * R) * F)) is Element of the carrier of G
K84( the carrier of G, the multF of G,F,((R ") * (((F ") * R) * F))) is Element of the carrier of G
(F ") * (F * ((R ") * (((F ") * R) * F))) is Element of the carrier of G
K84( the carrier of G, the multF of G,(F "),(F * ((R ") * (((F ") * R) * F)))) is Element of the carrier of G
F * (R ") is Element of the carrier of G
K84( the carrier of G, the multF of G,F,(R ")) is Element of the carrier of G
(F * (R ")) * (((F ") * R) * F) is Element of the carrier of G
K84( the carrier of G, the multF of G,(F * (R ")),(((F ") * R) * F)) is Element of the carrier of G
(F ") * ((F * (R ")) * (((F ") * R) * F)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(F "),((F * (R ")) * (((F ") * R) * F))) is Element of the carrier of G
(F * (R ")) * ((F ") * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(F * (R ")),((F ") * R)) is Element of the carrier of G
((F * (R ")) * ((F ") * R)) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,((F * (R ")) * ((F ") * R)),F) is Element of the carrier of G
(F ") * (((F * (R ")) * ((F ") * R)) * F) is Element of the carrier of G
K84( the carrier of G, the multF of G,(F "),(((F * (R ")) * ((F ") * R)) * F)) is Element of the carrier of G
(F ") * ((F * (R ")) * ((F ") * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(F "),((F * (R ")) * ((F ") * R))) is Element of the carrier of G
((F ") * ((F * (R ")) * ((F ") * R))) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * ((F * (R ")) * ((F ") * R))),F) is Element of the carrier of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
F is Element of the carrier of G
R is Element of the carrier of G
R " is Element of the carrier of G
[.F,(R ").] is Element of the carrier of G
F " is Element of the carrier of G
(R ") " is Element of the carrier of G
(F ") * ((R ") ") is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) V22( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
K84( the carrier of G, the multF of G,(F "),((R ") ")) is Element of the carrier of G
((F ") * ((R ") ")) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * ((R ") ")),F) is Element of the carrier of G
(((F ") * ((R ") ")) * F) * (R ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(((F ") * ((R ") ")) * F),(R ")) is Element of the carrier of G
[.F,(R ").] |^ R is Element of the carrier of G
(R ") * [.F,(R ").] is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),[.F,(R ").]) is Element of the carrier of G
((R ") * [.F,(R ").]) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * [.F,(R ").]),R) is Element of the carrier of G
([.F,(R ").] |^ R) " is Element of the carrier of G
[.(R "),F.] is Element of the carrier of G
((R ") ") * (F ") is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") "),(F ")) is Element of the carrier of G
(((R ") ") * (F ")) * (R ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(((R ") ") * (F ")),(R ")) is Element of the carrier of G
((((R ") ") * (F ")) * (R ")) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,((((R ") ") * (F ")) * (R ")),F) is Element of the carrier of G
[.(R "),F.] |^ R is Element of the carrier of G
(R ") * [.(R "),F.] is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),[.(R "),F.]) is Element of the carrier of G
((R ") * [.(R "),F.]) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * [.(R "),F.]),R) is Element of the carrier of G
[.F,(R ").] " is Element of the carrier of G
([.F,(R ").] ") |^ R is Element of the carrier of G
(R ") * ([.F,(R ").] ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),([.F,(R ").] ")) is Element of the carrier of G
((R ") * ([.F,(R ").] ")) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * ([.F,(R ").] ")),R) is Element of the carrier of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
F is Element of the carrier of G
R is Element of the carrier of G
R " is Element of the carrier of G
[.F,(R ").] is Element of the carrier of G
F " is Element of the carrier of G
(R ") " is Element of the carrier of G
(F ") * ((R ") ") is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) V22( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
K84( the carrier of G, the multF of G,(F "),((R ") ")) is Element of the carrier of G
((F ") * ((R ") ")) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * ((R ") ")),F) is Element of the carrier of G
(((F ") * ((R ") ")) * F) * (R ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(((F ") * ((R ") ")) * F),(R ")) is Element of the carrier of G
[.F,(R ").] |^ R is Element of the carrier of G
(R ") * [.F,(R ").] is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),[.F,(R ").]) is Element of the carrier of G
((R ") * [.F,(R ").]) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * [.F,(R ").]),R) is Element of the carrier of G
c4 is Element of the carrier of G
[.F,(R "),c4.] is Element of the carrier of G
[.[.F,(R ").],c4.] is Element of the carrier of G
[.F,(R ").] " is Element of the carrier of G
c4 " is Element of the carrier of G
([.F,(R ").] ") * (c4 ") is Element of the carrier of G
K84( the carrier of G, the multF of G,([.F,(R ").] "),(c4 ")) is Element of the carrier of G
(([.F,(R ").] ") * (c4 ")) * [.F,(R ").] is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.F,(R ").] ") * (c4 ")),[.F,(R ").]) is Element of the carrier of G
((([.F,(R ").] ") * (c4 ")) * [.F,(R ").]) * c4 is Element of the carrier of G
K84( the carrier of G, the multF of G,((([.F,(R ").] ") * (c4 ")) * [.F,(R ").]),c4) is Element of the carrier of G
[.F,(R "),c4.] |^ R is Element of the carrier of G
(R ") * [.F,(R "),c4.] is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),[.F,(R "),c4.]) is Element of the carrier of G
((R ") * [.F,(R "),c4.]) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * [.F,(R "),c4.]),R) is Element of the carrier of G
c4 |^ R is Element of the carrier of G
(R ") * c4 is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),c4) is Element of the carrier of G
((R ") * c4) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * c4),R) is Element of the carrier of G
[.([.F,(R ").] |^ R),(c4 |^ R).] is Element of the carrier of G
([.F,(R ").] |^ R) " is Element of the carrier of G
(c4 |^ R) " is Element of the carrier of G
(([.F,(R ").] |^ R) ") * ((c4 |^ R) ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.F,(R ").] |^ R) "),((c4 |^ R) ")) is Element of the carrier of G
((([.F,(R ").] |^ R) ") * ((c4 |^ R) ")) * ([.F,(R ").] |^ R) is Element of the carrier of G
K84( the carrier of G, the multF of G,((([.F,(R ").] |^ R) ") * ((c4 |^ R) ")),([.F,(R ").] |^ R)) is Element of the carrier of G
(((([.F,(R ").] |^ R) ") * ((c4 |^ R) ")) * ([.F,(R ").] |^ R)) * (c4 |^ R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(((([.F,(R ").] |^ R) ") * ((c4 |^ R) ")) * ([.F,(R ").] |^ R)),(c4 |^ R)) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
([.F,(R ").] ") * (1_ G) is Element of the carrier of G
K84( the carrier of G, the multF of G,([.F,(R ").] "),(1_ G)) is Element of the carrier of G
(([.F,(R ").] ") * (1_ G)) * (c4 ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.F,(R ").] ") * (1_ G)),(c4 ")) is Element of the carrier of G
((([.F,(R ").] ") * (1_ G)) * (c4 ")) * [.F,(R ").] is Element of the carrier of G
K84( the carrier of G, the multF of G,((([.F,(R ").] ") * (1_ G)) * (c4 ")),[.F,(R ").]) is Element of the carrier of G
(((([.F,(R ").] ") * (1_ G)) * (c4 ")) * [.F,(R ").]) * c4 is Element of the carrier of G
K84( the carrier of G, the multF of G,(((([.F,(R ").] ") * (1_ G)) * (c4 ")) * [.F,(R ").]),c4) is Element of the carrier of G
(R ") * ((((([.F,(R ").] ") * (1_ G)) * (c4 ")) * [.F,(R ").]) * c4) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),((((([.F,(R ").] ") * (1_ G)) * (c4 ")) * [.F,(R ").]) * c4)) is Element of the carrier of G
((R ") * ((((([.F,(R ").] ") * (1_ G)) * (c4 ")) * [.F,(R ").]) * c4)) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * ((((([.F,(R ").] ") * (1_ G)) * (c4 ")) * [.F,(R ").]) * c4)),R) is Element of the carrier of G
R * (R ") is Element of the carrier of G
K84( the carrier of G, the multF of G,R,(R ")) is Element of the carrier of G
([.F,(R ").] ") * (R * (R ")) is Element of the carrier of G
K84( the carrier of G, the multF of G,([.F,(R ").] "),(R * (R "))) is Element of the carrier of G
(([.F,(R ").] ") * (R * (R "))) * (c4 ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.F,(R ").] ") * (R * (R "))),(c4 ")) is Element of the carrier of G
((([.F,(R ").] ") * (R * (R "))) * (c4 ")) * [.F,(R ").] is Element of the carrier of G
K84( the carrier of G, the multF of G,((([.F,(R ").] ") * (R * (R "))) * (c4 ")),[.F,(R ").]) is Element of the carrier of G
(((([.F,(R ").] ") * (R * (R "))) * (c4 ")) * [.F,(R ").]) * c4 is Element of the carrier of G
K84( the carrier of G, the multF of G,(((([.F,(R ").] ") * (R * (R "))) * (c4 ")) * [.F,(R ").]),c4) is Element of the carrier of G
(R ") * ((((([.F,(R ").] ") * (R * (R "))) * (c4 ")) * [.F,(R ").]) * c4) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),((((([.F,(R ").] ") * (R * (R "))) * (c4 ")) * [.F,(R ").]) * c4)) is Element of the carrier of G
((R ") * ((((([.F,(R ").] ") * (R * (R "))) * (c4 ")) * [.F,(R ").]) * c4)) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * ((((([.F,(R ").] ") * (R * (R "))) * (c4 ")) * [.F,(R ").]) * c4)),R) is Element of the carrier of G
([.F,(R ").] ") * R is Element of the carrier of G
K84( the carrier of G, the multF of G,([.F,(R ").] "),R) is Element of the carrier of G
(([.F,(R ").] ") * R) * (R ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.F,(R ").] ") * R),(R ")) is Element of the carrier of G
((([.F,(R ").] ") * R) * (R ")) * (c4 ") is Element of the carrier of G
K84( the carrier of G, the multF of G,((([.F,(R ").] ") * R) * (R ")),(c4 ")) is Element of the carrier of G
(((([.F,(R ").] ") * R) * (R ")) * (c4 ")) * [.F,(R ").] is Element of the carrier of G
K84( the carrier of G, the multF of G,(((([.F,(R ").] ") * R) * (R ")) * (c4 ")),[.F,(R ").]) is Element of the carrier of G
((((([.F,(R ").] ") * R) * (R ")) * (c4 ")) * [.F,(R ").]) * c4 is Element of the carrier of G
K84( the carrier of G, the multF of G,((((([.F,(R ").] ") * R) * (R ")) * (c4 ")) * [.F,(R ").]),c4) is Element of the carrier of G
(R ") * (((((([.F,(R ").] ") * R) * (R ")) * (c4 ")) * [.F,(R ").]) * c4) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),(((((([.F,(R ").] ") * R) * (R ")) * (c4 ")) * [.F,(R ").]) * c4)) is Element of the carrier of G
((R ") * (((((([.F,(R ").] ") * R) * (R ")) * (c4 ")) * [.F,(R ").]) * c4)) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (((((([.F,(R ").] ") * R) * (R ")) * (c4 ")) * [.F,(R ").]) * c4)),R) is Element of the carrier of G
[.F,(R ").] * c4 is Element of the carrier of G
K84( the carrier of G, the multF of G,[.F,(R ").],c4) is Element of the carrier of G
(((([.F,(R ").] ") * R) * (R ")) * (c4 ")) * ([.F,(R ").] * c4) is Element of the carrier of G
K84( the carrier of G, the multF of G,(((([.F,(R ").] ") * R) * (R ")) * (c4 ")),([.F,(R ").] * c4)) is Element of the carrier of G
(R ") * ((((([.F,(R ").] ") * R) * (R ")) * (c4 ")) * ([.F,(R ").] * c4)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),((((([.F,(R ").] ") * R) * (R ")) * (c4 ")) * ([.F,(R ").] * c4))) is Element of the carrier of G
((R ") * ((((([.F,(R ").] ") * R) * (R ")) * (c4 ")) * ([.F,(R ").] * c4))) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * ((((([.F,(R ").] ") * R) * (R ")) * (c4 ")) * ([.F,(R ").] * c4))),R) is Element of the carrier of G
(c4 ") * ([.F,(R ").] * c4) is Element of the carrier of G
K84( the carrier of G, the multF of G,(c4 "),([.F,(R ").] * c4)) is Element of the carrier of G
((([.F,(R ").] ") * R) * (R ")) * ((c4 ") * ([.F,(R ").] * c4)) is Element of the carrier of G
K84( the carrier of G, the multF of G,((([.F,(R ").] ") * R) * (R ")),((c4 ") * ([.F,(R ").] * c4))) is Element of the carrier of G
(R ") * (((([.F,(R ").] ") * R) * (R ")) * ((c4 ") * ([.F,(R ").] * c4))) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),(((([.F,(R ").] ") * R) * (R ")) * ((c4 ") * ([.F,(R ").] * c4)))) is Element of the carrier of G
((R ") * (((([.F,(R ").] ") * R) * (R ")) * ((c4 ") * ([.F,(R ").] * c4)))) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (((([.F,(R ").] ") * R) * (R ")) * ((c4 ") * ([.F,(R ").] * c4)))),R) is Element of the carrier of G
(R ") * ((c4 ") * ([.F,(R ").] * c4)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),((c4 ") * ([.F,(R ").] * c4))) is Element of the carrier of G
(([.F,(R ").] ") * R) * ((R ") * ((c4 ") * ([.F,(R ").] * c4))) is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.F,(R ").] ") * R),((R ") * ((c4 ") * ([.F,(R ").] * c4)))) is Element of the carrier of G
(R ") * ((([.F,(R ").] ") * R) * ((R ") * ((c4 ") * ([.F,(R ").] * c4)))) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),((([.F,(R ").] ") * R) * ((R ") * ((c4 ") * ([.F,(R ").] * c4))))) is Element of the carrier of G
((R ") * ((([.F,(R ").] ") * R) * ((R ") * ((c4 ") * ([.F,(R ").] * c4))))) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * ((([.F,(R ").] ") * R) * ((R ") * ((c4 ") * ([.F,(R ").] * c4))))),R) is Element of the carrier of G
(R ") * (([.F,(R ").] ") * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),(([.F,(R ").] ") * R)) is Element of the carrier of G
((R ") * (([.F,(R ").] ") * R)) * ((R ") * ((c4 ") * ([.F,(R ").] * c4))) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (([.F,(R ").] ") * R)),((R ") * ((c4 ") * ([.F,(R ").] * c4)))) is Element of the carrier of G
(((R ") * (([.F,(R ").] ") * R)) * ((R ") * ((c4 ") * ([.F,(R ").] * c4)))) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,(((R ") * (([.F,(R ").] ") * R)) * ((R ") * ((c4 ") * ([.F,(R ").] * c4)))),R) is Element of the carrier of G
([.F,(R ").] ") |^ R is Element of the carrier of G
(R ") * ([.F,(R ").] ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),([.F,(R ").] ")) is Element of the carrier of G
((R ") * ([.F,(R ").] ")) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * ([.F,(R ").] ")),R) is Element of the carrier of G
(([.F,(R ").] ") |^ R) * ((R ") * ((c4 ") * ([.F,(R ").] * c4))) is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.F,(R ").] ") |^ R),((R ") * ((c4 ") * ([.F,(R ").] * c4)))) is Element of the carrier of G
((([.F,(R ").] ") |^ R) * ((R ") * ((c4 ") * ([.F,(R ").] * c4)))) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((([.F,(R ").] ") |^ R) * ((R ") * ((c4 ") * ([.F,(R ").] * c4)))),R) is Element of the carrier of G
((R ") * ((c4 ") * ([.F,(R ").] * c4))) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * ((c4 ") * ([.F,(R ").] * c4))),R) is Element of the carrier of G
(([.F,(R ").] ") |^ R) * (((R ") * ((c4 ") * ([.F,(R ").] * c4))) * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.F,(R ").] ") |^ R),(((R ") * ((c4 ") * ([.F,(R ").] * c4))) * R)) is Element of the carrier of G
[.F,(R ").] |^ c4 is Element of the carrier of G
(c4 ") * [.F,(R ").] is Element of the carrier of G
K84( the carrier of G, the multF of G,(c4 "),[.F,(R ").]) is Element of the carrier of G
((c4 ") * [.F,(R ").]) * c4 is Element of the carrier of G
K84( the carrier of G, the multF of G,((c4 ") * [.F,(R ").]),c4) is Element of the carrier of G
([.F,(R ").] |^ c4) |^ R is Element of the carrier of G
(R ") * ([.F,(R ").] |^ c4) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),([.F,(R ").] |^ c4)) is Element of the carrier of G
((R ") * ([.F,(R ").] |^ c4)) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * ([.F,(R ").] |^ c4)),R) is Element of the carrier of G
(([.F,(R ").] ") |^ R) * (([.F,(R ").] |^ c4) |^ R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.F,(R ").] ") |^ R),(([.F,(R ").] |^ c4) |^ R)) is Element of the carrier of G
[.(R "),F.] is Element of the carrier of G
((R ") ") * (F ") is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") "),(F ")) is Element of the carrier of G
(((R ") ") * (F ")) * (R ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(((R ") ") * (F ")),(R ")) is Element of the carrier of G
((((R ") ") * (F ")) * (R ")) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,((((R ") ") * (F ")) * (R ")),F) is Element of the carrier of G
[.(R "),F.] |^ R is Element of the carrier of G
(R ") * [.(R "),F.] is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),[.(R "),F.]) is Element of the carrier of G
((R ") * [.(R "),F.]) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * [.(R "),F.]),R) is Element of the carrier of G
([.(R "),F.] |^ R) * (([.F,(R ").] |^ c4) |^ R) is Element of the carrier of G
K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),(([.F,(R ").] |^ c4) |^ R)) is Element of the carrier of G
c4 * R is Element of the carrier of G
K84( the carrier of G, the multF of G,c4,R) is Element of the carrier of G
[.F,(R ").] |^ (c4 * R) is Element of the carrier of G
(c4 * R) " is Element of the carrier of G
((c4 * R) ") * [.F,(R ").] is Element of the carrier of G
K84( the carrier of G, the multF of G,((c4 * R) "),[.F,(R ").]) is Element of the carrier of G
(((c4 * R) ") * [.F,(R ").]) * (c4 * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(((c4 * R) ") * [.F,(R ").]),(c4 * R)) is Element of the carrier of G
([.(R "),F.] |^ R) * ([.F,(R ").] |^ (c4 * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),([.F,(R ").] |^ (c4 * R))) is Element of the carrier of G
([.(R "),F.] |^ R) * ((c4 |^ R) ") is Element of the carrier of G
K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),((c4 |^ R) ")) is Element of the carrier of G
(([.(R "),F.] |^ R) * ((c4 |^ R) ")) * ([.F,(R ").] |^ R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * ((c4 |^ R) ")),([.F,(R ").] |^ R)) is Element of the carrier of G
((([.(R "),F.] |^ R) * ((c4 |^ R) ")) * ([.F,(R ").] |^ R)) * (c4 |^ R) is Element of the carrier of G
K84( the carrier of G, the multF of G,((([.(R "),F.] |^ R) * ((c4 |^ R) ")) * ([.F,(R ").] |^ R)),(c4 |^ R)) is Element of the carrier of G
(c4 ") |^ R is Element of the carrier of G
(R ") * (c4 ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),(c4 ")) is Element of the carrier of G
((R ") * (c4 ")) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (c4 ")),R) is Element of the carrier of G
([.(R "),F.] |^ R) * ((c4 ") |^ R) is Element of the carrier of G
K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),((c4 ") |^ R)) is Element of the carrier of G
(([.(R "),F.] |^ R) * ((c4 ") |^ R)) * ([.F,(R ").] |^ R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * ((c4 ") |^ R)),([.F,(R ").] |^ R)) is Element of the carrier of G
((([.(R "),F.] |^ R) * ((c4 ") |^ R)) * ([.F,(R ").] |^ R)) * (c4 |^ R) is Element of the carrier of G
K84( the carrier of G, the multF of G,((([.(R "),F.] |^ R) * ((c4 ") |^ R)) * ([.F,(R ").] |^ R)),(c4 |^ R)) is Element of the carrier of G
([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),(((R ") * (c4 ")) * R)) is Element of the carrier of G
(([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R)) * (((R ") * [.F,(R ").]) * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R)),(((R ") * [.F,(R ").]) * R)) is Element of the carrier of G
(R ") * (c4 * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),(c4 * R)) is Element of the carrier of G
((([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R)) * (((R ") * [.F,(R ").]) * R)) * ((R ") * (c4 * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,((([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R)) * (((R ") * [.F,(R ").]) * R)),((R ") * (c4 * R))) is Element of the carrier of G
(((R ") * [.F,(R ").]) * R) * ((R ") * (c4 * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(((R ") * [.F,(R ").]) * R),((R ") * (c4 * R))) is Element of the carrier of G
(([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R)) * ((((R ") * [.F,(R ").]) * R) * ((R ") * (c4 * R))) is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R)),((((R ") * [.F,(R ").]) * R) * ((R ") * (c4 * R)))) is Element of the carrier of G
R * ((R ") * (c4 * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,R,((R ") * (c4 * R))) is Element of the carrier of G
((R ") * [.F,(R ").]) * (R * ((R ") * (c4 * R))) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * [.F,(R ").]),(R * ((R ") * (c4 * R)))) is Element of the carrier of G
(([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R)) * (((R ") * [.F,(R ").]) * (R * ((R ") * (c4 * R)))) is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R)),(((R ") * [.F,(R ").]) * (R * ((R ") * (c4 * R))))) is Element of the carrier of G
(R * (R ")) * (c4 * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R * (R ")),(c4 * R)) is Element of the carrier of G
((R ") * [.F,(R ").]) * ((R * (R ")) * (c4 * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * [.F,(R ").]),((R * (R ")) * (c4 * R))) is Element of the carrier of G
(([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R)) * (((R ") * [.F,(R ").]) * ((R * (R ")) * (c4 * R))) is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R)),(((R ") * [.F,(R ").]) * ((R * (R ")) * (c4 * R)))) is Element of the carrier of G
(1_ G) * (c4 * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(1_ G),(c4 * R)) is Element of the carrier of G
((R ") * [.F,(R ").]) * ((1_ G) * (c4 * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * [.F,(R ").]),((1_ G) * (c4 * R))) is Element of the carrier of G
(([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R)) * (((R ") * [.F,(R ").]) * ((1_ G) * (c4 * R))) is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R)),(((R ") * [.F,(R ").]) * ((1_ G) * (c4 * R)))) is Element of the carrier of G
((R ") * [.F,(R ").]) * (c4 * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * [.F,(R ").]),(c4 * R)) is Element of the carrier of G
(([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R)) * (((R ") * [.F,(R ").]) * (c4 * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * (((R ") * (c4 ")) * R)),(((R ") * [.F,(R ").]) * (c4 * R))) is Element of the carrier of G
(((R ") * (c4 ")) * R) * (((R ") * [.F,(R ").]) * (c4 * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(((R ") * (c4 ")) * R),(((R ") * [.F,(R ").]) * (c4 * R))) is Element of the carrier of G
([.(R "),F.] |^ R) * ((((R ") * (c4 ")) * R) * (((R ") * [.F,(R ").]) * (c4 * R))) is Element of the carrier of G
K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),((((R ") * (c4 ")) * R) * (((R ") * [.F,(R ").]) * (c4 * R)))) is Element of the carrier of G
R * (((R ") * [.F,(R ").]) * (c4 * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,R,(((R ") * [.F,(R ").]) * (c4 * R))) is Element of the carrier of G
((R ") * (c4 ")) * (R * (((R ") * [.F,(R ").]) * (c4 * R))) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (c4 ")),(R * (((R ") * [.F,(R ").]) * (c4 * R)))) is Element of the carrier of G
([.(R "),F.] |^ R) * (((R ") * (c4 ")) * (R * (((R ") * [.F,(R ").]) * (c4 * R)))) is Element of the carrier of G
K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),(((R ") * (c4 ")) * (R * (((R ") * [.F,(R ").]) * (c4 * R))))) is Element of the carrier of G
R * ((R ") * [.F,(R ").]) is Element of the carrier of G
K84( the carrier of G, the multF of G,R,((R ") * [.F,(R ").])) is Element of the carrier of G
(R * ((R ") * [.F,(R ").])) * (c4 * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R * ((R ") * [.F,(R ").])),(c4 * R)) is Element of the carrier of G
((R ") * (c4 ")) * ((R * ((R ") * [.F,(R ").])) * (c4 * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (c4 ")),((R * ((R ") * [.F,(R ").])) * (c4 * R))) is Element of the carrier of G
([.(R "),F.] |^ R) * (((R ") * (c4 ")) * ((R * ((R ") * [.F,(R ").])) * (c4 * R))) is Element of the carrier of G
K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),(((R ") * (c4 ")) * ((R * ((R ") * [.F,(R ").])) * (c4 * R)))) is Element of the carrier of G
(R * (R ")) * [.F,(R ").] is Element of the carrier of G
K84( the carrier of G, the multF of G,(R * (R ")),[.F,(R ").]) is Element of the carrier of G
((R * (R ")) * [.F,(R ").]) * (c4 * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R * (R ")) * [.F,(R ").]),(c4 * R)) is Element of the carrier of G
((R ") * (c4 ")) * (((R * (R ")) * [.F,(R ").]) * (c4 * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (c4 ")),(((R * (R ")) * [.F,(R ").]) * (c4 * R))) is Element of the carrier of G
([.(R "),F.] |^ R) * (((R ") * (c4 ")) * (((R * (R ")) * [.F,(R ").]) * (c4 * R))) is Element of the carrier of G
K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),(((R ") * (c4 ")) * (((R * (R ")) * [.F,(R ").]) * (c4 * R)))) is Element of the carrier of G
(1_ G) * [.F,(R ").] is Element of the carrier of G
K84( the carrier of G, the multF of G,(1_ G),[.F,(R ").]) is Element of the carrier of G
((1_ G) * [.F,(R ").]) * (c4 * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,((1_ G) * [.F,(R ").]),(c4 * R)) is Element of the carrier of G
((R ") * (c4 ")) * (((1_ G) * [.F,(R ").]) * (c4 * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (c4 ")),(((1_ G) * [.F,(R ").]) * (c4 * R))) is Element of the carrier of G
([.(R "),F.] |^ R) * (((R ") * (c4 ")) * (((1_ G) * [.F,(R ").]) * (c4 * R))) is Element of the carrier of G
K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),(((R ") * (c4 ")) * (((1_ G) * [.F,(R ").]) * (c4 * R)))) is Element of the carrier of G
[.F,(R ").] * (c4 * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,[.F,(R ").],(c4 * R)) is Element of the carrier of G
((R ") * (c4 ")) * ([.F,(R ").] * (c4 * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (c4 ")),([.F,(R ").] * (c4 * R))) is Element of the carrier of G
([.(R "),F.] |^ R) * (((R ") * (c4 ")) * ([.F,(R ").] * (c4 * R))) is Element of the carrier of G
K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),(((R ") * (c4 ")) * ([.F,(R ").] * (c4 * R)))) is Element of the carrier of G
((R ") * (c4 ")) * [.F,(R ").] is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (c4 ")),[.F,(R ").]) is Element of the carrier of G
(((R ") * (c4 ")) * [.F,(R ").]) * (c4 * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(((R ") * (c4 ")) * [.F,(R ").]),(c4 * R)) is Element of the carrier of G
([.(R "),F.] |^ R) * ((((R ") * (c4 ")) * [.F,(R ").]) * (c4 * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),((((R ") * (c4 ")) * [.F,(R ").]) * (c4 * R))) is Element of the carrier of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
F is Element of the carrier of G
R is Element of the carrier of G
R " is Element of the carrier of G
[.F,(R ").] is Element of the carrier of G
F " is Element of the carrier of G
(R ") " is Element of the carrier of G
(F ") * ((R ") ") is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) V22( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
K84( the carrier of G, the multF of G,(F "),((R ") ")) is Element of the carrier of G
((F ") * ((R ") ")) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,((F ") * ((R ") ")),F) is Element of the carrier of G
(((F ") * ((R ") ")) * F) * (R ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(((F ") * ((R ") ")) * F),(R ")) is Element of the carrier of G
[.F,(R ").] |^ R is Element of the carrier of G
(R ") * [.F,(R ").] is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),[.F,(R ").]) is Element of the carrier of G
((R ") * [.F,(R ").]) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * [.F,(R ").]),R) is Element of the carrier of G
[.R,F.] is Element of the carrier of G
(R ") * (F ") is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),(F ")) is Element of the carrier of G
((R ") * (F ")) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (F ")),R) is Element of the carrier of G
(((R ") * (F ")) * R) * F is Element of the carrier of G
K84( the carrier of G, the multF of G,(((R ") * (F ")) * R),F) is Element of the carrier of G
((((F ") * ((R ") ")) * F) * (R ")) * R is Element of the carrier of G
K84( the carrier of G, the multF of G,((((F ") * ((R ") ")) * F) * (R ")),R) is Element of the carrier of G
(R ") * (((((F ") * ((R ") ")) * F) * (R ")) * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),(((((F ") * ((R ") ")) * F) * (R ")) * R)) is Element of the carrier of G
(R ") * R is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),R) is Element of the carrier of G
(((F ") * ((R ") ")) * F) * ((R ") * R) is Element of the carrier of G
K84( the carrier of G, the multF of G,(((F ") * ((R ") ")) * F),((R ") * R)) is Element of the carrier of G
(R ") * ((((F ") * ((R ") ")) * F) * ((R ") * R)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),((((F ") * ((R ") ")) * F) * ((R ") * R))) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(((F ") * ((R ") ")) * F) * (1_ G) is Element of the carrier of G
K84( the carrier of G, the multF of G,(((F ") * ((R ") ")) * F),(1_ G)) is Element of the carrier of G
(R ") * ((((F ") * ((R ") ")) * F) * (1_ G)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),((((F ") * ((R ") ")) * F) * (1_ G))) is Element of the carrier of G
(R ") * (((F ") * ((R ") ")) * F) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),(((F ") * ((R ") ")) * F)) is Element of the carrier of G
R * F is Element of the carrier of G
K84( the carrier of G, the multF of G,R,F) is Element of the carrier of G
(F ") * (R * F) is Element of the carrier of G
K84( the carrier of G, the multF of G,(F "),(R * F)) is Element of the carrier of G
(R ") * ((F ") * (R * F)) is Element of the carrier of G
K84( the carrier of G, the multF of G,(R "),((F ") * (R * F))) is Element of the carrier of G
((R ") * (F ")) * (R * F) is Element of the carrier of G
K84( the carrier of G, the multF of G,((R ") * (F ")),(