:: GRNILP_1 semantic presentation

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

{ b

{1} is non empty set

Seg 2 is non empty V37() V44(2) Element of bool NAT

{ b

{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

c

[.F,(R "),c

[.[.F,(R ").],c

[.F,(R ").] " is Element of the carrier of G

c

([.F,(R ").] ") * (c

K84( the carrier of G, the multF of G,([.F,(R ").] "),(c

(([.F,(R ").] ") * (c

K84( the carrier of G, the multF of G,(([.F,(R ").] ") * (c

((([.F,(R ").] ") * (c

K84( the carrier of G, the multF of G,((([.F,(R ").] ") * (c

[.F,(R "),c

(R ") * [.F,(R "),c

K84( the carrier of G, the multF of G,(R "),[.F,(R "),c

((R ") * [.F,(R "),c

K84( the carrier of G, the multF of G,((R ") * [.F,(R "),c

c

(R ") * c

K84( the carrier of G, the multF of G,(R "),c

((R ") * c

K84( the carrier of G, the multF of G,((R ") * c

[.([.F,(R ").] |^ R),(c

([.F,(R ").] |^ R) " is Element of the carrier of G

(c

(([.F,(R ").] |^ R) ") * ((c

K84( the carrier of G, the multF of G,(([.F,(R ").] |^ R) "),((c

((([.F,(R ").] |^ R) ") * ((c

K84( the carrier of G, the multF of G,((([.F,(R ").] |^ R) ") * ((c

(((([.F,(R ").] |^ R) ") * ((c

K84( the carrier of G, the multF of G,(((([.F,(R ").] |^ R) ") * ((c

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)) * (c

K84( the carrier of G, the multF of G,(([.F,(R ").] ") * (1_ G)),(c

((([.F,(R ").] ") * (1_ G)) * (c

K84( the carrier of G, the multF of G,((([.F,(R ").] ") * (1_ G)) * (c

(((([.F,(R ").] ") * (1_ G)) * (c

K84( the carrier of G, the multF of G,(((([.F,(R ").] ") * (1_ G)) * (c

(R ") * ((((([.F,(R ").] ") * (1_ G)) * (c

K84( the carrier of G, the multF of G,(R "),((((([.F,(R ").] ") * (1_ G)) * (c

((R ") * ((((([.F,(R ").] ") * (1_ G)) * (c

K84( the carrier of G, the multF of G,((R ") * ((((([.F,(R ").] ") * (1_ G)) * (c

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 "))) * (c

K84( the carrier of G, the multF of G,(([.F,(R ").] ") * (R * (R "))),(c

((([.F,(R ").] ") * (R * (R "))) * (c

K84( the carrier of G, the multF of G,((([.F,(R ").] ") * (R * (R "))) * (c

(((([.F,(R ").] ") * (R * (R "))) * (c

K84( the carrier of G, the multF of G,(((([.F,(R ").] ") * (R * (R "))) * (c

(R ") * ((((([.F,(R ").] ") * (R * (R "))) * (c

K84( the carrier of G, the multF of G,(R "),((((([.F,(R ").] ") * (R * (R "))) * (c

((R ") * ((((([.F,(R ").] ") * (R * (R "))) * (c

K84( the carrier of G, the multF of G,((R ") * ((((([.F,(R ").] ") * (R * (R "))) * (c

([.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 ")) * (c

K84( the carrier of G, the multF of G,((([.F,(R ").] ") * R) * (R ")),(c

(((([.F,(R ").] ") * R) * (R ")) * (c

K84( the carrier of G, the multF of G,(((([.F,(R ").] ") * R) * (R ")) * (c

((((([.F,(R ").] ") * R) * (R ")) * (c

K84( the carrier of G, the multF of G,((((([.F,(R ").] ") * R) * (R ")) * (c

(R ") * (((((([.F,(R ").] ") * R) * (R ")) * (c

K84( the carrier of G, the multF of G,(R "),(((((([.F,(R ").] ") * R) * (R ")) * (c

((R ") * (((((([.F,(R ").] ") * R) * (R ")) * (c

K84( the carrier of G, the multF of G,((R ") * (((((([.F,(R ").] ") * R) * (R ")) * (c

[.F,(R ").] * c

K84( the carrier of G, the multF of G,[.F,(R ").],c

(((([.F,(R ").] ") * R) * (R ")) * (c

K84( the carrier of G, the multF of G,(((([.F,(R ").] ") * R) * (R ")) * (c

(R ") * ((((([.F,(R ").] ") * R) * (R ")) * (c

K84( the carrier of G, the multF of G,(R "),((((([.F,(R ").] ") * R) * (R ")) * (c

((R ") * ((((([.F,(R ").] ") * R) * (R ")) * (c

K84( the carrier of G, the multF of G,((R ") * ((((([.F,(R ").] ") * R) * (R ")) * (c

(c

K84( the carrier of G, the multF of G,(c

((([.F,(R ").] ") * R) * (R ")) * ((c

K84( the carrier of G, the multF of G,((([.F,(R ").] ") * R) * (R ")),((c

(R ") * (((([.F,(R ").] ") * R) * (R ")) * ((c

K84( the carrier of G, the multF of G,(R "),(((([.F,(R ").] ") * R) * (R ")) * ((c

((R ") * (((([.F,(R ").] ") * R) * (R ")) * ((c

K84( the carrier of G, the multF of G,((R ") * (((([.F,(R ").] ") * R) * (R ")) * ((c

(R ") * ((c

K84( the carrier of G, the multF of G,(R "),((c

(([.F,(R ").] ") * R) * ((R ") * ((c

K84( the carrier of G, the multF of G,(([.F,(R ").] ") * R),((R ") * ((c

(R ") * ((([.F,(R ").] ") * R) * ((R ") * ((c

K84( the carrier of G, the multF of G,(R "),((([.F,(R ").] ") * R) * ((R ") * ((c

((R ") * ((([.F,(R ").] ") * R) * ((R ") * ((c

K84( the carrier of G, the multF of G,((R ") * ((([.F,(R ").] ") * R) * ((R ") * ((c

(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 ") * ((c

K84( the carrier of G, the multF of G,((R ") * (([.F,(R ").] ") * R)),((R ") * ((c

(((R ") * (([.F,(R ").] ") * R)) * ((R ") * ((c

K84( the carrier of G, the multF of G,(((R ") * (([.F,(R ").] ") * R)) * ((R ") * ((c

([.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 ") * ((c

K84( the carrier of G, the multF of G,(([.F,(R ").] ") |^ R),((R ") * ((c

((([.F,(R ").] ") |^ R) * ((R ") * ((c

K84( the carrier of G, the multF of G,((([.F,(R ").] ") |^ R) * ((R ") * ((c

((R ") * ((c

K84( the carrier of G, the multF of G,((R ") * ((c

(([.F,(R ").] ") |^ R) * (((R ") * ((c

K84( the carrier of G, the multF of G,(([.F,(R ").] ") |^ R),(((R ") * ((c

[.F,(R ").] |^ c

(c

K84( the carrier of G, the multF of G,(c

((c

K84( the carrier of G, the multF of G,((c

([.F,(R ").] |^ c

(R ") * ([.F,(R ").] |^ c

K84( the carrier of G, the multF of G,(R "),([.F,(R ").] |^ c

((R ") * ([.F,(R ").] |^ c

K84( the carrier of G, the multF of G,((R ") * ([.F,(R ").] |^ c

(([.F,(R ").] ") |^ R) * (([.F,(R ").] |^ c

K84( the carrier of G, the multF of G,(([.F,(R ").] ") |^ R),(([.F,(R ").] |^ c

[.(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 ").] |^ c

K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),(([.F,(R ").] |^ c

c

K84( the carrier of G, the multF of G,c

[.F,(R ").] |^ (c

(c

((c

K84( the carrier of G, the multF of G,((c

(((c

K84( the carrier of G, the multF of G,(((c

([.(R "),F.] |^ R) * ([.F,(R ").] |^ (c

K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),([.F,(R ").] |^ (c

([.(R "),F.] |^ R) * ((c

K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),((c

(([.(R "),F.] |^ R) * ((c

K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * ((c

((([.(R "),F.] |^ R) * ((c

K84( the carrier of G, the multF of G,((([.(R "),F.] |^ R) * ((c

(c

(R ") * (c

K84( the carrier of G, the multF of G,(R "),(c

((R ") * (c

K84( the carrier of G, the multF of G,((R ") * (c

([.(R "),F.] |^ R) * ((c

K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),((c

(([.(R "),F.] |^ R) * ((c

K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * ((c

((([.(R "),F.] |^ R) * ((c

K84( the carrier of G, the multF of G,((([.(R "),F.] |^ R) * ((c

([.(R "),F.] |^ R) * (((R ") * (c

K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),(((R ") * (c

(([.(R "),F.] |^ R) * (((R ") * (c

K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * (((R ") * (c

(R ") * (c

K84( the carrier of G, the multF of G,(R "),(c

((([.(R "),F.] |^ R) * (((R ") * (c

K84( the carrier of G, the multF of G,((([.(R "),F.] |^ R) * (((R ") * (c

(((R ") * [.F,(R ").]) * R) * ((R ") * (c

K84( the carrier of G, the multF of G,(((R ") * [.F,(R ").]) * R),((R ") * (c

(([.(R "),F.] |^ R) * (((R ") * (c

K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * (((R ") * (c

R * ((R ") * (c

K84( the carrier of G, the multF of G,R,((R ") * (c

((R ") * [.F,(R ").]) * (R * ((R ") * (c

K84( the carrier of G, the multF of G,((R ") * [.F,(R ").]),(R * ((R ") * (c

(([.(R "),F.] |^ R) * (((R ") * (c

K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * (((R ") * (c

(R * (R ")) * (c

K84( the carrier of G, the multF of G,(R * (R ")),(c

((R ") * [.F,(R ").]) * ((R * (R ")) * (c

K84( the carrier of G, the multF of G,((R ") * [.F,(R ").]),((R * (R ")) * (c

(([.(R "),F.] |^ R) * (((R ") * (c

K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * (((R ") * (c

(1_ G) * (c

K84( the carrier of G, the multF of G,(1_ G),(c

((R ") * [.F,(R ").]) * ((1_ G) * (c

K84( the carrier of G, the multF of G,((R ") * [.F,(R ").]),((1_ G) * (c

(([.(R "),F.] |^ R) * (((R ") * (c

K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * (((R ") * (c

((R ") * [.F,(R ").]) * (c

K84( the carrier of G, the multF of G,((R ") * [.F,(R ").]),(c

(([.(R "),F.] |^ R) * (((R ") * (c

K84( the carrier of G, the multF of G,(([.(R "),F.] |^ R) * (((R ") * (c

(((R ") * (c

K84( the carrier of G, the multF of G,(((R ") * (c

([.(R "),F.] |^ R) * ((((R ") * (c

K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),((((R ") * (c

R * (((R ") * [.F,(R ").]) * (c

K84( the carrier of G, the multF of G,R,(((R ") * [.F,(R ").]) * (c

((R ") * (c

K84( the carrier of G, the multF of G,((R ") * (c

([.(R "),F.] |^ R) * (((R ") * (c

K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),(((R ") * (c

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 ").])) * (c

K84( the carrier of G, the multF of G,(R * ((R ") * [.F,(R ").])),(c

((R ") * (c

K84( the carrier of G, the multF of G,((R ") * (c

([.(R "),F.] |^ R) * (((R ") * (c

K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),(((R ") * (c

(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 ").]) * (c

K84( the carrier of G, the multF of G,((R * (R ")) * [.F,(R ").]),(c

((R ") * (c

K84( the carrier of G, the multF of G,((R ") * (c

([.(R "),F.] |^ R) * (((R ") * (c

K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),(((R ") * (c

(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 ").]) * (c

K84( the carrier of G, the multF of G,((1_ G) * [.F,(R ").]),(c

((R ") * (c

K84( the carrier of G, the multF of G,((R ") * (c

([.(R "),F.] |^ R) * (((R ") * (c

K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),(((R ") * (c

[.F,(R ").] * (c

K84( the carrier of G, the multF of G,[.F,(R ").],(c

((R ") * (c

K84( the carrier of G, the multF of G,((R ") * (c

([.(R "),F.] |^ R) * (((R ") * (c

K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),(((R ") * (c

((R ") * (c

K84( the carrier of G, the multF of G,((R ") * (c

(((R ") * (c

K84( the carrier of G, the multF of G,(((R ") * (c

([.(R "),F.] |^ R) * ((((R ") * (c

K84( the carrier of G, the multF of G,([.(R "),F.] |^ R),((((R ") * (c

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 ")),(