:: 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₁}) where b₁ is Relation-like vR -defined n -valued Function-like quasi_total Element of Funcs (vR,n) : verum } is set
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₁ where b₁ is Element of the carrier of R : Z * b₁ = b₁ * Z } is set
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₁ where b₁ is Element of the carrier of R : Z * b₁ = b₁ * Z } is set
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₁ where b₁ is Element of the carrier of R : Z * b₁ = b₁ * Z } is set
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₁ |^ b₂) where b₁, b₂ is Element of the carrier of R : ( b₁ in K462( the carrier of R,Z) & b₂ in carr ((Omega). R) ) } 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 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₁ |^ b₂) where b₁, b₂ is Element of the carrier of R : ( b₁ in K462( the carrier of R,Z) & b₂ in carr ((Omega). R) ) } is set
[: 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<