:: WEDDWITT semantic presentation

REAL is non empty non trivial non finite set

NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty non trivial non finite set

F_Complex is non empty non degenerated non trivial right_complementable almost_left_invertible strict Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

the carrier of F_Complex is non empty non trivial set

COMPLEX is non empty non trivial non finite set

NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal set

bool NAT is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

[:NAT,REAL:] is non empty non trivial non finite set

bool [:NAT,REAL:] is non empty non trivial non finite set

RAT is non empty non trivial non finite set

INT is non empty non trivial non finite set

[:REAL,REAL:] is non empty non trivial non finite set

bool [:REAL,REAL:] is non empty non trivial non finite set

{} is V6() V7() V8() V10() V11() V12() Function-like functional empty V31() V32() integer finite V39() cardinal {} -element FinSequence-membered ext-real non positive non negative set

1 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

{{},1} is non empty finite V39() set

K397() is set

bool K397() is non empty set

K398() is Element of bool K397()

2 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

[:2,2:] is non empty finite set

[:[:2,2:],2:] is non empty finite set

bool [:[:2,2:],2:] is non empty finite V39() set

K548() is non empty strict multMagma

the carrier of K548() is non empty set

K553() is non empty strict unital Group-like associative commutative V190() V191() V192() V193() V194() V195() multMagma

K554() is non empty strict associative commutative V193() V194() V195() M35(K553())

K555() is non empty strict unital associative commutative V193() V194() V195() V196() M38(K553(),K554())

K557() is non empty strict unital associative commutative multMagma

K558() is non empty strict unital associative commutative V196() M35(K557())

1 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT

bool the carrier of F_Complex is non empty set

[:NAT, the carrier of F_Complex:] is non empty non trivial non finite set

bool [:NAT, the carrier of F_Complex:] is non empty non trivial non finite set

[:COMPLEX,COMPLEX:] is non empty non trivial non finite set

bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set

[:[:REAL,REAL:],REAL:] is non empty non trivial non finite set

bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set

[:RAT,RAT:] is non empty non trivial non finite set

bool [:RAT,RAT:] is non empty non trivial non finite set

[:[:RAT,RAT:],RAT:] is non empty non trivial non finite set

bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set

[:INT,INT:] is non empty non trivial non finite set

bool [:INT,INT:] is non empty non trivial non finite set

[:[:INT,INT:],INT:] is non empty non trivial non finite set

bool [:[:INT,INT:],INT:] is non empty non trivial non finite set

[:NAT,NAT:] is non empty non trivial non finite set

[:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

3 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

0 is V6() V7() V8() V10() V11() V12() Function-like functional empty V31() V32() integer finite V39() cardinal {} -element FinSequence-membered ext-real non positive non negative Element of NAT

card {} is V6() V7() V8() V10() V11() V12() Function-like functional empty V31() V32() integer finite V39() cardinal {} -element FinSequence-membered ext-real non positive non negative set

Seg 1 is non empty trivial finite 1 -element Element of bool NAT

K692() is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like quasi_total V62() Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]

K694() is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like quasi_total V62() Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]

K122() is Element of COMPLEX

K121() is V6() V7() V8() V10() V11() V12() Function-like functional empty V31() V32() integer finite V39() cardinal {} -element FinSequence-membered ext-real non positive non negative Element of COMPLEX

<*> REAL is Relation-like NAT -defined REAL -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty proper V31() V32() integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V62() V63() V64() V65() Function-yielding V84() FinSequence of REAL

Sum (<*> REAL) is V31() V32() ext-real Element of REAL

{{}} is non empty trivial finite V39() 1 -element set

R is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Z is V31() V32() ext-real Element of REAL

Z |^ R is V31() V32() ext-real Element of REAL

1 + 1 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

0 + 1 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

Z #Z R is V31() V32() ext-real Element of REAL

Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative set

R is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative set

R * Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative set

cZ is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative set

(R * Z) + cZ is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative set

Z -' 1 is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R * (Z -' 1) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(R * (Z -' 1)) + cZ is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

q is V31() V32() ext-real Element of REAL

q |^ ((R * Z) + cZ) is V31() V32() ext-real Element of REAL

q |^ R is V31() V32() ext-real Element of REAL

q |^ ((R * (Z -' 1)) + cZ) is V31() V32() ext-real Element of REAL

(q |^ R) * (q |^ ((R * (Z -' 1)) + cZ)) is V31() V32() ext-real set

0 + 1 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

(Z -' 1) + 1 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

R + ((R * (Z -' 1)) + cZ) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

q #Z (R + ((R * (Z -' 1)) + cZ)) is V31() V32() ext-real Element of REAL

q #Z R is V31() V32() ext-real Element of REAL

q #Z ((R * (Z -' 1)) + cZ) is V31() V32() ext-real Element of REAL

(q #Z R) * (q #Z ((R * (Z -' 1)) + cZ)) is V31() V32() ext-real set

(q |^ R) * (q #Z ((R * (Z -' 1)) + cZ)) is V31() V32() ext-real set

Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R |^ Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(R |^ Z) -' 1 is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

cZ is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R |^ cZ is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(R |^ cZ) -' 1 is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

cZ mod Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R |^ (cZ mod Z) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

cZ div Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Z * (cZ div Z) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(Z * (cZ div Z)) + (cZ mod Z) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Rs is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative set

Z * Rs is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(Z * Rs) + (cZ mod Z) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R |^ ((Z * Rs) + (cZ mod Z)) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(R |^ ((Z * Rs) + (cZ mod Z))) -' 1 is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(R |^ (cZ mod Z)) -' 1 is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

cR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative set

(cZ mod Z) + cR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R |^ ((cZ mod Z) + cR) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R #Z ((cZ mod Z) + cR) is V31() V32() ext-real Element of REAL

R #Z (cZ mod Z) is V31() V32() ext-real Element of REAL

R #Z cR is V31() V32() ext-real Element of REAL

(R #Z (cZ mod Z)) * (R #Z cR) is V31() V32() ext-real set

R |^ cR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of REAL

0 + 1 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

(R |^ Z) - 1 is V31() V32() integer ext-real set

- 1 is V31() V32() integer ext-real non positive set

(R |^ Z) + (- 1) is V31() V32() integer ext-real set

(R |^ (cZ mod Z)) - 1 is V31() V32() integer ext-real set

(R |^ (cZ mod Z)) + (- 1) is V31() V32() integer ext-real set

((R |^ (cZ mod Z)) - 1) + 1 is V31() V32() integer ext-real set

cR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative set

cR + 1 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

Rs - 1 is V31() V32() integer ext-real set

0 + 1 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

Rs -' 1 is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Z * cR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(Z * cR) + (cZ mod Z) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R |^ ((Z * cR) + (cZ mod Z)) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Z * (Rs -' 1) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(Z * (Rs -' 1)) + (cZ mod Z) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R |^ ((Z * (Rs -' 1)) + (cZ mod Z)) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(R |^ ((Z * cR) + (cZ mod Z))) -' 1 is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

- ((R |^ Z) -' 1) is V31() V32() integer ext-real non positive set

((R |^ ((Z * Rs) + (cZ mod Z))) -' 1) + (- ((R |^ Z) -' 1)) is V31() V32() integer ext-real set

(R |^ ((Z * Rs) + (cZ mod Z))) - 1 is V31() V32() integer ext-real set

(R |^ Z) - 1 is V31() V32() integer ext-real set

((R |^ ((Z * Rs) + (cZ mod Z))) - 1) - ((R |^ Z) - 1) is V31() V32() integer ext-real set

(R |^ ((Z * Rs) + (cZ mod Z))) - (R |^ Z) is V31() V32() integer ext-real set

(R |^ Z) * (R |^ ((Z * (Rs -' 1)) + (cZ mod Z))) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(R |^ Z) * 1 is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

((R |^ Z) * (R |^ ((Z * (Rs -' 1)) + (cZ mod Z)))) - ((R |^ Z) * 1) is V31() V32() integer ext-real set

((R |^ ((Z * Rs) + (cZ mod Z))) -' 1) - ((R |^ Z) -' 1) is V31() V32() integer ext-real set

(R |^ ((Z * (Rs -' 1)) + (cZ mod Z))) - 1 is V31() V32() integer ext-real set

(R |^ Z) * ((R |^ ((Z * (Rs -' 1)) + (cZ mod Z))) - 1) is V31() V32() integer ext-real set

(R |^ ((Z * (Rs -' 1)) + (cZ mod Z))) -' 1 is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(R |^ Z) * ((R |^ ((Z * (Rs -' 1)) + (cZ mod Z))) -' 1) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

((R |^ Z) -' 1) + 1 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative set

R is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative set

Funcs (R,Z) is set

card (Funcs (R,Z)) is V6() V7() V8() cardinal set

Z |^ R is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative set

cZ is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Funcs ({},cZ) is set

Funcs (0,cZ) is set

card (Funcs (0,cZ)) is V6() V7() V8() cardinal set

cZ #Z 0 is V31() V32() ext-real Element of REAL

cZ |^ 0 is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

cZ |^ 0 is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of REAL

q is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative set

Funcs (q,cZ) is set

card (Funcs (q,cZ)) is V6() V7() V8() cardinal set

cZ |^ q is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of REAL

q + 1 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

Funcs ((q + 1),cZ) is set

card (Funcs ((q + 1),cZ)) is V6() V7() V8() cardinal set

cZ |^ (q + 1) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of REAL

vR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

vR + 1 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

[:(vR + 1),cZ:] is finite set

bool [:(vR + 1),cZ:] is non empty finite V39() set

n is non empty set

Funcs ((vR + 1),n) is non empty FUNCTION_DOMAIN of vR + 1,n

Funcs (vR,n) is non empty FUNCTION_DOMAIN of vR,n

Rs is set

cR is Relation-like Function-like set

dom cR is set

rng cR is set

[:(vR + 1),n:] is non empty set

bool [:(vR + 1),n:] is non empty set

{vR} is non empty trivial finite V39() 1 -element set

(vR + 1) /\ vR is finite set

vR \/ {vR} is non empty finite set

(vR \/ {vR}) /\ vR is finite set

vR /\ vR is finite set

{vR} /\ vR is finite set

(vR /\ vR) \/ ({vR} /\ vR) is finite set

vR \/ {} is finite set

cRs is Relation-like vR + 1 -defined n -valued Function-like quasi_total finite Element of bool [:(vR + 1),n:]

cRs | vR is Relation-like vR + 1 -defined n -valued Function-like finite Element of bool [:(vR + 1),n:]

dom (cRs | vR) is finite Element of bool (vR + 1)

bool (vR + 1) is non empty finite V39() set

rng (cRs | vR) is finite Element of bool n

bool n is non empty set

[:(Funcs ((vR + 1),n)),(Funcs (vR,n)):] is non empty set

bool [:(Funcs ((vR + 1),n)),(Funcs (vR,n)):] is non empty set

Rs is Relation-like Funcs ((vR + 1),n) -defined Funcs (vR,n) -valued Function-like quasi_total Element of bool [:(Funcs ((vR + 1),n)),(Funcs (vR,n)):]

rng Rs is Element of bool (Funcs (vR,n))

bool (Funcs (vR,n)) is non empty set

cR is set

cRs is set

cZs is Relation-like vR -defined n -valued Function-like quasi_total Element of Funcs (vR,n)

vR .--> cRs is Relation-like NAT -defined {vR} -defined Function-like one-to-one finite set

{vR} is non empty trivial finite V39() 1 -element set

{vR} --> cRs is Relation-like {vR} -defined {cRs} -valued Function-like constant non empty total quasi_total finite Element of bool [:{vR},{cRs}:]

{cRs} is non empty trivial finite 1 -element set

[:{vR},{cRs}:] is non empty finite set

bool [:{vR},{cRs}:] is non empty finite V39() set

cZs +* (vR .--> cRs) is Relation-like Function-like set

{cZs} is functional non empty trivial finite 1 -element set

Rs " {cZs} is Element of bool (Funcs ((vR + 1),n))

bool (Funcs ((vR + 1),n)) is non empty set

A is set

vR .--> A is Relation-like NAT -defined {vR} -defined Function-like one-to-one finite set

{vR} --> A is Relation-like {vR} -defined {A} -valued Function-like constant non empty total quasi_total finite Element of bool [:{vR},{A}:]

{A} is non empty trivial finite 1 -element set

[:{vR},{A}:] is non empty finite set

bool [:{vR},{A}:] is non empty finite V39() set

cZs +* (vR .--> A) is Relation-like Function-like set

B is Relation-like Function-like set

dom cZs is finite Element of bool vR

bool vR is non empty finite V39() set

dom (vR .--> A) is trivial finite V39() Element of bool {vR}

bool {vR} is non empty finite V39() set

dom B is set

vR \/ {vR} is non empty finite set

rng (vR .--> A) is finite set

rng B is set

rng cZs is Element of bool n

bool n is non empty set

(rng cZs) \/ {A} is non empty set

Funcs ((vR + 1),cZ) is set

f is Relation-like vR + 1 -defined cZ -valued Function-like quasi_total finite Element of bool [:(vR + 1),cZ:]

f | vR is Relation-like vR + 1 -defined cZ -valued Function-like finite Element of bool [:(vR + 1),cZ:]

Rs . f is set

{cR} is non empty trivial finite 1 -element set

f1 is Relation-like vR + 1 -defined cZ -valued Function-like quasi_total finite Element of bool [:(vR + 1),cZ:]

f1 | vR is Relation-like vR + 1 -defined cZ -valued Function-like finite Element of bool [:(vR + 1),cZ:]

dom Rs is Element of bool (Funcs ((vR + 1),n))

A is set

[(cZs +* (vR .--> cRs)),A] is set

{(cZs +* (vR .--> cRs)),A} is non empty finite set

{(cZs +* (vR .--> cRs))} is functional non empty trivial finite 1 -element set

{{(cZs +* (vR .--> cRs)),A},{(cZs +* (vR .--> cRs))}} is non empty finite V39() set

dom Rs is Element of bool (Funcs ((vR + 1),n))

Rs . (cZs +* (vR .--> cRs)) is set

(cZs +* (vR .--> cRs)) | vR is Relation-like Function-like finite set

B is Relation-like vR + 1 -defined cZ -valued Function-like quasi_total finite Element of bool [:(vR + 1),cZ:]

B | vR is Relation-like vR + 1 -defined cZ -valued Function-like finite Element of bool [:(vR + 1),cZ:]

dom cZs is finite Element of bool vR

bool vR is non empty finite V39() set

dom (vR .--> cRs) is trivial finite V39() Element of bool {vR}

bool {vR} is non empty finite V39() set

cR is Relation-like vR -defined n -valued Function-like quasi_total Element of Funcs (vR,n)

{cR} is functional non empty trivial finite 1 -element set

Rs " {cR} is Element of bool (Funcs ((vR + 1),n))

bool (Funcs ((vR + 1),n)) is non empty set

card (Rs " {cR}) is V6() V7() V8() cardinal set

cRs is set

vR .--> cRs is Relation-like NAT -defined {vR} -defined Function-like one-to-one finite set

{vR} is non empty trivial finite V39() 1 -element set

{vR} --> cRs is Relation-like {vR} -defined {cRs} -valued Function-like constant non empty total quasi_total finite Element of bool [:{vR},{cRs}:]

{cRs} is non empty trivial finite 1 -element set

[:{vR},{cRs}:] is non empty finite set

bool [:{vR},{cRs}:] is non empty finite V39() set

cR +* (vR .--> cRs) is Relation-like Function-like set

cZs is Relation-like Function-like set

dom cR is finite Element of bool vR

bool vR is non empty finite V39() set

dom (vR .--> cRs) is trivial finite V39() Element of bool {vR}

bool {vR} is non empty finite V39() set

dom cZs is set

vR \/ {vR} is non empty finite set

rng (vR .--> cRs) is finite set

rng cZs is set

rng cR is Element of bool n

bool n is non empty set

(rng cR) \/ {cRs} is non empty set

Funcs ((vR + 1),cZ) is set

natq1 is Relation-like vR + 1 -defined cZ -valued Function-like quasi_total finite Element of bool [:(vR + 1),cZ:]

natq1 | vR is Relation-like vR + 1 -defined cZ -valued Function-like finite Element of bool [:(vR + 1),cZ:]

Rs . natq1 is set

A is Relation-like vR + 1 -defined cZ -valued Function-like quasi_total finite Element of bool [:(vR + 1),cZ:]

A | vR is Relation-like vR + 1 -defined cZ -valued Function-like finite Element of bool [:(vR + 1),cZ:]

dom Rs is Element of bool (Funcs ((vR + 1),n))

[:cZ,(Rs " {cR}):] is set

bool [:cZ,(Rs " {cR}):] is non empty set

cRs is Relation-like cZ -defined Rs " {cR} -valued Function-like quasi_total finite Element of bool [:cZ,(Rs " {cR}):]

cZs is set

[:(vR + 1),n:] is non empty set

bool [:(vR + 1),n:] is non empty set

Rs . cZs is set

natq1 is Relation-like vR + 1 -defined n -valued Function-like quasi_total finite Element of bool [:(vR + 1),n:]

natq1 | vR is Relation-like vR + 1 -defined n -valued Function-like finite Element of bool [:(vR + 1),n:]

natq1 . vR is set

A is set

cRs . A is set

{vR} is non empty trivial finite V39() 1 -element set

vR \/ {vR} is non empty finite set

dom natq1 is finite Element of bool (vR + 1)

bool (vR + 1) is non empty finite V39() set

vR .--> (natq1 . vR) is Relation-like NAT -defined {vR} -defined Function-like one-to-one finite set

{vR} --> (natq1 . vR) is Relation-like {vR} -defined {(natq1 . vR)} -valued Function-like constant non empty total quasi_total finite Element of bool [:{vR},{(natq1 . vR)}:]

{(natq1 . vR)} is non empty trivial finite 1 -element set

[:{vR},{(natq1 . vR)}:] is non empty finite set

bool [:{vR},{(natq1 . vR)}:] is non empty finite V39() set

(natq1 | vR) +* (vR .--> (natq1 . vR)) is Relation-like Function-like finite set

rng cRs is finite Element of bool (Rs " {cR})

bool (Rs " {cR}) is non empty set

dom cRs is finite Element of bool cZ

bool cZ is non empty finite V39() set

cZs is set

natq1 is set

cRs . cZs is set

cRs . natq1 is set

vR .--> natq1 is Relation-like NAT -defined {vR} -defined Function-like one-to-one finite set

{vR} is non empty trivial finite V39() 1 -element set

{vR} --> natq1 is Relation-like {vR} -defined {natq1} -valued Function-like constant non empty total quasi_total finite Element of bool [:{vR},{natq1}:]

{natq1} is non empty trivial finite 1 -element set

[:{vR},{natq1}:] is non empty finite set

bool [:{vR},{natq1}:] is non empty finite V39() set

cR +* (vR .--> natq1) is Relation-like Function-like set

vR .--> cZs is Relation-like NAT -defined {vR} -defined Function-like one-to-one finite set

{vR} --> cZs is Relation-like {vR} -defined {cZs} -valued Function-like constant non empty total quasi_total finite Element of bool [:{vR},{cZs}:]

{cZs} is non empty trivial finite 1 -element set

[:{vR},{cZs}:] is non empty finite set

bool [:{vR},{cZs}:] is non empty finite V39() set

dom (vR .--> cZs) is trivial finite V39() Element of bool {vR}

bool {vR} is non empty finite V39() set

dom (vR .--> natq1) is trivial finite V39() Element of bool {vR}

cR +* (vR .--> cZs) is Relation-like Function-like set

(vR .--> cZs) . vR is set

(vR .--> natq1) . vR is set

(cR +* (vR .--> cZs)) . vR is set

cRs .: cZ is finite Element of bool (Rs " {cR})

cR is set

cRs is set

{cR} is non empty trivial finite 1 -element set

Rs " {cR} is Element of bool (Funcs ((vR + 1),n))

bool (Funcs ((vR + 1),n)) is non empty set

{cRs} is non empty trivial finite 1 -element set

Rs " {cRs} is Element of bool (Funcs ((vR + 1),n))

(Rs " {cR}) /\ (Rs " {cRs}) is Element of bool (Funcs ((vR + 1),n))

cZs is set

Rs . cZs is set

natq1 is Relation-like vR + 1 -defined cZ -valued Function-like quasi_total finite Element of bool [:(vR + 1),cZ:]

Funcs ((vR + 1),cZ) is set

Rs . natq1 is set

natq1 | vR is Relation-like vR + 1 -defined cZ -valued Function-like finite Element of bool [:(vR + 1),cZ:]

A is Relation-like vR + 1 -defined cZ -valued Function-like quasi_total finite Element of bool [:(vR + 1),cZ:]

A | vR is Relation-like vR + 1 -defined cZ -valued Function-like finite Element of bool [:(vR + 1),cZ:]

A is Relation-like vR + 1 -defined cZ -valued Function-like quasi_total finite Element of bool [:(vR + 1),cZ:]

A | vR is Relation-like vR + 1 -defined cZ -valued Function-like finite Element of bool [:(vR + 1),cZ:]

{ (Rs " {b

cR is set

union cR is set

Funcs ((vR + 1),cZ) is set

cRs is set

cZs is set

Funcs (vR,cZ) is set

natq1 is Element of Funcs (vR,cZ)

{natq1} is non empty trivial finite 1 -element set

Rs " {natq1} is Element of bool (Funcs ((vR + 1),n))

bool (Funcs ((vR + 1),n)) is non empty set

cRs is set

Rs . cRs is set

cZs is Relation-like vR + 1 -defined cZ -valued Function-like quasi_total finite Element of bool [:(vR + 1),cZ:]

cZs | vR is Relation-like vR + 1 -defined cZ -valued Function-like finite Element of bool [:(vR + 1),cZ:]

dom Rs is Element of bool (Funcs ((vR + 1),n))

bool (Funcs ((vR + 1),n)) is non empty set

Rs . cZs is set

{(cZs | vR)} is functional non empty trivial finite V39() 1 -element set

Rs " {(cZs | vR)} is Element of bool (Funcs ((vR + 1),n))

natq1 is set

A is Relation-like vR + 1 -defined cZ -valued Function-like quasi_total finite Element of bool [:(vR + 1),cZ:]

A | vR is Relation-like vR + 1 -defined cZ -valued Function-like finite Element of bool [:(vR + 1),cZ:]

cRs is finite set

card cRs is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

cZ |^ vR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

bool (Funcs ((vR + 1),n)) is non empty set

Funcs (vR,cZ) is set

cZs is set

{cZs} is non empty trivial finite 1 -element set

Rs " {cZs} is Element of bool (Funcs ((vR + 1),n))

[:(Funcs (vR,cZ)),cRs:] is set

bool [:(Funcs (vR,cZ)),cRs:] is non empty set

cZs is Relation-like Funcs (vR,cZ) -defined cRs -valued Function-like quasi_total Element of bool [:(Funcs (vR,cZ)),cRs:]

natq1 is set

A is Element of Funcs (vR,cZ)

{A} is non empty trivial finite 1 -element set

Rs " {A} is Element of bool (Funcs ((vR + 1),n))

cZs . A is set

the Relation-like vR -defined n -valued Function-like quasi_total Element of Funcs (vR,n) is Relation-like vR -defined n -valued Function-like quasi_total Element of Funcs (vR,n)

{ the Relation-like vR -defined n -valued Function-like quasi_total Element of Funcs (vR,n)} is functional non empty trivial finite 1 -element set

Rs " { the Relation-like vR -defined n -valued Function-like quasi_total Element of Funcs (vR,n)} is Element of bool (Funcs ((vR + 1),n))

rng cZs is finite Element of bool cRs

bool cRs is non empty finite V39() set

dom cZs is Element of bool (Funcs (vR,cZ))

bool (Funcs (vR,cZ)) is non empty set

A is set

B is set

cZs . A is set

cZs . B is set

{A} is non empty trivial finite 1 -element set

Rs " {A} is Element of bool (Funcs ((vR + 1),n))

{B} is non empty trivial finite 1 -element set

Rs " {B} is Element of bool (Funcs ((vR + 1),n))

(Rs " {A}) /\ (Rs " {A}) is Element of bool (Funcs ((vR + 1),n))

cZs .: (Funcs (vR,cZ)) is finite Element of bool cRs

cZs is set

natq1 is Relation-like vR -defined n -valued Function-like quasi_total Element of Funcs (vR,n)

{natq1} is functional non empty trivial finite 1 -element set

Rs " {natq1} is Element of bool (Funcs ((vR + 1),n))

bool (Funcs ((vR + 1),n)) is non empty set

card cZs is V6() V7() V8() cardinal set

A is set

B is Relation-like vR -defined n -valued Function-like quasi_total Element of Funcs (vR,n)

{B} is functional non empty trivial finite 1 -element set

Rs " {B} is Element of bool (Funcs ((vR + 1),n))

card A is V6() V7() V8() cardinal set

union cRs is set

cZ * (card cRs) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

cZs is finite set

card cZs is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V62() V63() V64() V65() FinSequence of NAT

len R is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

dom R is finite Element of bool NAT

Sum R is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

<*> NAT is Relation-like NAT -defined NAT -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty proper V31() V32() integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V62() V63() V64() V65() Function-yielding V84() FinSequence of NAT

Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R + 1 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

Z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V62() V63() V64() V65() FinSequence of NAT

len Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

dom Z is finite Element of bool NAT

Sum Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

cZ is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

vR is set

<*vR*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set

q ^ <*vR*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V62() V63() V64() V65() FinSequence of NAT

len n is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Rs is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V62() V63() V64() V65() FinSequence of NAT

len Rs is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(len n) + (len Rs) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(len n) + 1 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

dom n is finite Element of bool NAT

cR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

n /. cR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Z /. cR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Z . cR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of REAL

n . cR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of REAL

Sum n is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

rng Rs is finite V72() V73() V74() V77() Element of bool REAL

{vR} is non empty trivial finite 1 -element set

Z . (len Z) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of REAL

cR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Seg (len Z) is finite len Z -element Element of bool NAT

Z /. (len Z) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(Sum n) + cR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V62() V63() V64() V65() FinSequence of NAT

dom R is finite Element of bool NAT

Sum R is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

len R is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R is finite set

card R is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Z is finite V39() V50() a_partition of R

card Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

cZ is Relation-like NAT -defined Z -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Z

rng cZ is finite V39() Element of bool Z

bool Z is non empty finite V39() set

len cZ is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V62() V63() V64() V65() FinSequence of NAT

len q is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

dom q is finite Element of bool NAT

Sum q is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R + 1 is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

Z is finite set

card Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

cZ is finite V39() V50() a_partition of Z

card cZ is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

q is Relation-like NAT -defined cZ -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of cZ

rng q is finite V39() Element of bool cZ

bool cZ is non empty finite V39() set

len q is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

vR is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V62() V63() V64() V65() FinSequence of NAT

len vR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

dom vR is finite Element of bool NAT

Sum vR is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

n is non empty set

Rs is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of n

Seg R is finite R -element Element of bool NAT

Rs | (Seg R) is Relation-like NAT -defined n -valued Function-like finite FinSubsequence-like Element of bool [:NAT,n:]

[:NAT,n:] is non empty non trivial non finite set

bool [:NAT,n:] is non empty non trivial non finite set

cRs is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of n

len cRs is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Rs . (R + 1) is set

<*(Rs . (R + 1))*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set

cRs ^ <*(Rs . (R + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

rng cRs is finite Element of bool n

bool n is non empty set

cZs is finite set

natq1 is Relation-like NAT -defined cZs -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of cZs

card cZs is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

union cZs is set

A is finite set

bool A is non empty finite V39() set

B is finite Element of bool A

f is finite Element of bool A

f is finite Element of bool A

bool (union cZs) is non empty set

vR | (Seg R) is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite FinSubsequence-like V62() V63() V64() V65() Element of bool [:NAT,NAT:]

bool [:NAT,NAT:] is non empty non trivial non finite set

B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V62() V63() V64() V65() FinSequence of NAT

len B is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

len natq1 is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

dom B is finite Element of bool NAT

f is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

B . f is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of REAL

natq1 . f is set

card (natq1 . f) is V6() V7() V8() cardinal set

dom natq1 is finite Element of bool NAT

vR . f is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of REAL

Rs . f is set

card (Rs . f) is V6() V7() V8() cardinal set

card A is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Sum B is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

f is set

f1 is set

dom Rs is finite Element of bool NAT

len Rs is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Seg (len Rs) is finite len Rs -element Element of bool NAT

rng Rs is finite Element of bool n

dom natq1 is finite Element of bool NAT

f2 is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative set

natq1 . f2 is set

Seg (R + 1) is non empty finite R + 1 -element Element of bool NAT

Rs . f2 is set

dom Rs is finite Element of bool NAT

len Rs is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Seg (len Rs) is finite len Rs -element Element of bool NAT

rng Rs is finite Element of bool n

rng natq1 is finite Element of bool cZs

bool cZs is non empty finite V39() set

f1 is finite set

<*f1*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set

rng <*f1*> is trivial finite set

(rng natq1) \/ (rng <*f1*>) is finite set

{f1} is non empty trivial finite V39() 1 -element set

cZs \/ {f1} is non empty finite set

cR is non empty finite set

union n is set

union {f1} is finite set

(union cZs) \/ (union {f1}) is set

A \/ f1 is finite set

Seg (R + 1) is non empty finite R + 1 -element Element of bool NAT

rng B is finite V72() V73() V74() V77() Element of bool REAL

card cR is V6() V7() V8() V12() non empty V31() V32() integer finite cardinal ext-real positive non negative Element of NAT

card f1 is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

(Sum B) + (card f1) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

vR . (R + 1) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of REAL

(Sum B) + (vR . (R + 1)) is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

f2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V62() V63() V64() FinSequence of REAL

<*(vR . (R + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V62() V63() V64() V66() V67() V68() V69() FinSequence of REAL

f2 ^ <*(vR . (R + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V62() V63() V64() FinSequence of REAL

Sum (f2 ^ <*(vR . (R + 1))*>) is V31() V32() ext-real Element of REAL

R is finite set

card R is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

Z is finite V39() V50() a_partition of R

card Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

cZ is Relation-like NAT -defined Z -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Z

rng cZ is finite V39() Element of bool Z

bool Z is non empty finite V39() set

q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V62() V63() V64() V65() FinSequence of NAT

len q is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

len cZ is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

dom q is finite Element of bool NAT

Sum q is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT

R is non empty finite unital Group-like associative V190() V191() V192() V193() V194() V195() multMagma

center R is non empty finite strict unital Group-like associative V190() V191() V192() V193() V194() V195() Subgroup of R

R is non empty unital Group-like associative V190() V191() V192() V193() V194() V195() multMagma

the carrier of R is non empty set

Z is Element of the carrier of R

{ b

1_ R is Element of the carrier of R

Z * (1_ R) is Element of the carrier of R

the multF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (Z,(1_ R)) is Element of the carrier of R

[Z,(1_ R)] is set

{Z,(1_ R)} is non empty finite set

{Z} is non empty trivial finite 1 -element set

{{Z,(1_ R)},{Z}} is non empty finite V39() set

the multF of R . [Z,(1_ R)] is set

(1_ R) * Z is Element of the carrier of R

the multF of R . ((1_ R),Z) is Element of the carrier of R

[(1_ R),Z] is set

{(1_ R),Z} is non empty finite set

{(1_ R)} is non empty trivial finite 1 -element set

{{(1_ R),Z},{(1_ R)}} is non empty finite V39() set

the multF of R . [(1_ R),Z] is set

q is set

vR is Element of the carrier of R

Z * vR is Element of the carrier of R

the multF of R . (Z,vR) is Element of the carrier of R

[Z,vR] is set

{Z,vR} is non empty finite set

{{Z,vR},{Z}} is non empty finite V39() set

the multF of R . [Z,vR] is set

vR * Z is Element of the carrier of R

the multF of R . (vR,Z) is Element of the carrier of R

[vR,Z] is set

{vR,Z} is non empty finite set

{vR} is non empty trivial finite 1 -element set

{{vR,Z},{vR}} is non empty finite V39() set

the multF of R . [vR,Z] is set

bool the carrier of R is non empty set

q is Element of the carrier of R

vR is Element of the carrier of R

q * vR is Element of the carrier of R

the multF of R . (q,vR) is Element of the carrier of R

[q,vR] is set

{q,vR} is non empty finite set

{q} is non empty trivial finite 1 -element set

{{q,vR},{q}} is non empty finite V39() set

the multF of R . [q,vR] is set

Z * (q * vR) is Element of the carrier of R

the multF of R . (Z,(q * vR)) is Element of the carrier of R

[Z,(q * vR)] is set

{Z,(q * vR)} is non empty finite set

{{Z,(q * vR)},{Z}} is non empty finite V39() set

the multF of R . [Z,(q * vR)] is set

q * Z is Element of the carrier of R

the multF of R . (q,Z) is Element of the carrier of R

[q,Z] is set

{q,Z} is non empty finite set

{{q,Z},{q}} is non empty finite V39() set

the multF of R . [q,Z] is set

(q * Z) * vR is Element of the carrier of R

the multF of R . ((q * Z),vR) is Element of the carrier of R

[(q * Z),vR] is set

{(q * Z),vR} is non empty finite set

{(q * Z)} is non empty trivial finite 1 -element set

{{(q * Z),vR},{(q * Z)}} is non empty finite V39() set

the multF of R . [(q * Z),vR] is set

vR * Z is Element of the carrier of R

the multF of R . (vR,Z) is Element of the carrier of R

[vR,Z] is set

{vR,Z} is non empty finite set

{vR} is non empty trivial finite 1 -element set

{{vR,Z},{vR}} is non empty finite V39() set

the multF of R . [vR,Z] is set

q * (vR * Z) is Element of the carrier of R

the multF of R . (q,(vR * Z)) is Element of the carrier of R

[q,(vR * Z)] is set

{q,(vR * Z)} is non empty finite set

{{q,(vR * Z)},{q}} is non empty finite V39() set

the multF of R . [q,(vR * Z)] is set

(q * vR) * Z is Element of the carrier of R

the multF of R . ((q * vR),Z) is Element of the carrier of R

[(q * vR),Z] is set

{(q * vR),Z} is non empty finite set

{(q * vR)} is non empty trivial finite 1 -element set

{{(q * vR),Z},{(q * vR)}} is non empty finite V39() set

the multF of R . [(q * vR),Z] is set

n is Element of the carrier of R

n * Z is Element of the carrier of R

the multF of R . (n,Z) is Element of the carrier of R

[n,Z] is set

{n,Z} is non empty finite set

{n} is non empty trivial finite 1 -element set

{{n,Z},{n}} is non empty finite V39() set

the multF of R . [n,Z] is set

Z * n is Element of the carrier of R

the multF of R . (Z,n) is Element of the carrier of R

[Z,n] is set

{Z,n} is non empty finite set

{{Z,n},{Z}} is non empty finite V39() set

the multF of R . [Z,n] is set

n is Element of the carrier of R

n * Z is Element of the carrier of R

the multF of R . (n,Z) is Element of the carrier of R

[n,Z] is set

{n,Z} is non empty finite set

{n} is non empty trivial finite 1 -element set

{{n,Z},{n}} is non empty finite V39() set

the multF of R . [n,Z] is set

Z * n is Element of the carrier of R

the multF of R . (Z,n) is Element of the carrier of R

[Z,n] is set

{Z,n} is non empty finite set

{{Z,n},{Z}} is non empty finite V39() set

the multF of R . [Z,n] is set

q is Element of the carrier of R

q " is Element of the carrier of R

q * Z is Element of the carrier of R

the multF of R . (q,Z) is Element of the carrier of R

[q,Z] is set

{q,Z} is non empty finite set

{q} is non empty trivial finite 1 -element set

{{q,Z},{q}} is non empty finite V39() set

the multF of R . [q,Z] is set

(q ") * (q * Z) is Element of the carrier of R

the multF of R . ((q "),(q * Z)) is Element of the carrier of R

[(q "),(q * Z)] is set

{(q "),(q * Z)} is non empty finite set

{(q ")} is non empty trivial finite 1 -element set

{{(q "),(q * Z)},{(q ")}} is non empty finite V39() set

the multF of R . [(q "),(q * Z)] is set

Z * q is Element of the carrier of R

the multF of R . (Z,q) is Element of the carrier of R

[Z,q] is set

{Z,q} is non empty finite set

{{Z,q},{Z}} is non empty finite V39() set

the multF of R . [Z,q] is set

(Z * q) * (q ") is Element of the carrier of R

the multF of R . ((Z * q),(q ")) is Element of the carrier of R

[(Z * q),(q ")] is set

{(Z * q),(q ")} is non empty finite set

{(Z * q)} is non empty trivial finite 1 -element set

{{(Z * q),(q ")},{(Z * q)}} is non empty finite V39() set

the multF of R . [(Z * q),(q ")] is set

(q ") * ((Z * q) * (q ")) is Element of the carrier of R

the multF of R . ((q "),((Z * q) * (q "))) is Element of the carrier of R

[(q "),((Z * q) * (q "))] is set

{(q "),((Z * q) * (q "))} is non empty finite set

{{(q "),((Z * q) * (q "))},{(q ")}} is non empty finite V39() set

the multF of R . [(q "),((Z * q) * (q "))] is set

Z * (q ") is Element of the carrier of R

the multF of R . (Z,(q ")) is Element of the carrier of R

[Z,(q ")] is set

{Z,(q ")} is non empty finite set

{{Z,(q ")},{Z}} is non empty finite V39() set

the multF of R . [Z,(q ")] is set

vR is Element of the carrier of R

vR * Z is Element of the carrier of R

the multF of R . (vR,Z) is Element of the carrier of R

[vR,Z] is set

{vR,Z} is non empty finite set

{vR} is non empty trivial finite 1 -element set

{{vR,Z},{vR}} is non empty finite V39() set

the multF of R . [vR,Z] is set

Z * vR is Element of the carrier of R

the multF of R . (Z,vR) is Element of the carrier of R

[Z,vR] is set

{Z,vR} is non empty finite set

{{Z,vR},{Z}} is non empty finite V39() set

the multF of R . [Z,vR] is set

(q ") * Z is Element of the carrier of R

the multF of R . ((q "),Z) is Element of the carrier of R

[(q "),Z] is set

{(q "),Z} is non empty finite set

{{(q "),Z},{(q ")}} is non empty finite V39() set

the multF of R . [(q "),Z] is set

cZ is non empty strict unital Group-like associative V190() V191() V192() V193() V194() V195() Subgroup of R

the carrier of cZ is non empty set

q is non empty strict unital Group-like associative V190() V191() V192() V193() V194() V195() Subgroup of R

the carrier of q is non empty set

vR is Element of the carrier of R

R is non empty finite unital Group-like associative V190() V191() V192() V193() V194() V195() multMagma

the carrier of R is non empty finite set

Z is Element of the carrier of R

(R,Z) is non empty finite strict unital Group-like associative V190() V191() V192() V193() V194() V195() Subgroup of R

R is non empty unital Group-like associative V190() V191() V192() V193() V194() V195() multMagma

the carrier of R is non empty set

Z is Element of the carrier of R

(R,Z) is non empty strict unital Group-like associative V190() V191() V192() V193() V194() V195() Subgroup of R

cZ is set

the carrier of (R,Z) is non empty set

{ b

q is Element of the carrier of R

Z * q is Element of the carrier of R

the multF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (Z,q) is Element of the carrier of R

[Z,q] is set

{Z,q} is non empty finite set

{Z} is non empty trivial finite 1 -element set

{{Z,q},{Z}} is non empty finite V39() set

the multF of R . [Z,q] is set

q * Z is Element of the carrier of R

the multF of R . (q,Z) is Element of the carrier of R

[q,Z] is set

{q,Z} is non empty finite set

{q} is non empty trivial finite 1 -element set

{{q,Z},{q}} is non empty finite V39() set

the multF of R . [q,Z] is set

R is non empty unital Group-like associative V190() V191() V192() V193() V194() V195() multMagma

the carrier of R is non empty set

Z is Element of the carrier of R

cZ is Element of the carrier of R

Z * cZ is Element of the carrier of R

the multF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

the multF of R . (Z,cZ) is Element of the carrier of R

[Z,cZ] is set

{Z,cZ} is non empty finite set

{Z} is non empty trivial finite 1 -element set

{{Z,cZ},{Z}} is non empty finite V39() set

the multF of R . [Z,cZ] is set

cZ * Z is Element of the carrier of R

the multF of R . (cZ,Z) is Element of the carrier of R

[cZ,Z] is set

{cZ,Z} is non empty finite set

{cZ} is non empty trivial finite 1 -element set

{{cZ,Z},{cZ}} is non empty finite V39() set

the multF of R . [cZ,Z] is set

(R,Z) is non empty strict unital Group-like associative V190() V191() V192() V193() V194() V195() Subgroup of R

the carrier of (R,Z) is non empty set

{ b

q is Element of the carrier of R

Z * q is Element of the carrier of R

the multF of R . (Z,q) is Element of the carrier of R

[Z,q] is set

{Z,q} is non empty finite set

{{Z,q},{Z}} is non empty finite V39() set

the multF of R . [Z,q] is set

q * Z is Element of the carrier of R

the multF of R . (q,Z) is Element of the carrier of R

[q,Z] is set

{q,Z} is non empty finite set

{q} is non empty trivial finite 1 -element set

{{q,Z},{q}} is non empty finite V39() set

the multF of R . [q,Z] is set

R is non empty unital Group-like associative V190() V191() V192() V193() V194() V195() multMagma

the carrier of R is non empty set

Z is Element of the carrier of R

con_class Z is Element of bool the carrier of R

bool the carrier of R is non empty set

(Omega). R is non empty strict unital Group-like associative V190() V191() V192() V193() V194() V195() Subgroup of R

the multF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

multMagma(# the carrier of R, the multF of R #) is non empty strict multMagma

carr ((Omega). R) is Element of bool the carrier of R

the carrier of ((Omega). R) is non empty set

Z |^ (carr ((Omega). R)) is Element of bool the carrier of R

K462( the carrier of R,Z) is non empty trivial finite 1 -element Element of bool the carrier of R

K462( the carrier of R,Z) |^ (carr ((Omega). R)) is Element of bool the carrier of R

{ (b

R is non empty unital Group-like associative V190() V191() V192() V193() V194() V195() multMagma

the carrier of R is non empty set

Z is Element of the carrier of R

con_class Z is non empty Element of bool the carrier of R

bool the carrier of R is non empty set

(Omega). R is non empty strict unital Group-like associative V190() V191() V192() V193() V194() V195() Subgroup of R

the multF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty set

[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set

multMagma(# the carrier of R, the multF of R #) is non empty strict multMagma

carr ((Omega). R) is Element of bool the carrier of R

the carrier of ((Omega). R) is non empty set

Z |^ (carr ((Omega). R)) is Element of bool the carrier of R

K462( the carrier of R,Z) is non empty trivial finite 1 -element Element of bool the carrier of R

K462( the carrier of R,Z) |^ (carr ((Omega). R)) is Element of bool the carrier of R

{ (b

[: the carrier of R,(con_class Z):] is non empty set

bool [: the carrier of R,(con_class Z):] is non empty set

cZ is Element of the carrier of R

Z |^ cZ is Element of the carrier of R

cZ " is Element of the carrier of R

(cZ ") * Z is Element of the carrier of R

the multF of R . ((cZ "),Z) is Element of the carrier of R

[(cZ "),Z] is set

{(cZ "),Z} is non empty finite set

{(cZ ")} is non empty trivial finite 1 -element set

{{(cZ "),Z},{(cZ ")}} is non empty finite V39() set

the multF of R . [(cZ "),Z] is set

((cZ ") * Z) * cZ is Element of the carrier of R

the multF of R . (((cZ ") * Z),cZ) is Element of the carrier of R

[((cZ ") * Z),cZ] is set

{((cZ ") * Z),cZ} is non empty finite set

{((cZ ") * Z<