:: 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

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
is non empty non trivial non finite set
bool 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
is non empty non trivial non finite set
bool is non empty non trivial non finite 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())

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

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
is non empty non trivial non finite set
bool is non empty non trivial non finite set
is non empty non trivial non finite set
bool is non empty non trivial non finite set
is non empty non trivial non finite set
bool is non empty non trivial non finite set
is non empty non trivial non finite set
bool is non empty non trivial non finite set
is non empty non trivial non finite set
bool is non empty non trivial non finite set
is non empty non trivial non finite set
bool is non empty non trivial non finite set
is non empty non trivial non finite set
bool is non empty non trivial non finite set
is non empty non trivial non finite set
is non empty non trivial non finite set
bool 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

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

K122() is Element of COMPLEX

Sum () 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

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} is non empty trivial finite V39() 1 -element set

{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

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

{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

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

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} is non empty trivial finite V39() 1 -element set

{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

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 {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} 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

{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 " {b1}) where b1 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

{} is functional non empty trivial finite 1 -element set
Rs " {} 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

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

len R is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of 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
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

len Z is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of 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

vR is set

len n is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element 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

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

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

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

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

len q is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of 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

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

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

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

len cRs is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of NAT
Rs . (R + 1) is set

rng cRs is finite Element of bool n
bool n is non empty set
cZs is finite set

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

bool is non empty non trivial non finite set

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

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

(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

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

rng cZ is finite V39() Element of bool Z
bool Z 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
len cZ is V6() V7() V8() V12() V31() V32() integer finite cardinal ext-real non negative Element of 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
{ b1 where b1 is Element of the carrier of R : Z * b1 = b1 * 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
{ b1 where b1 is Element of the carrier of R : Z * b1 = b1 * 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
{ b1 where b1 is Element of the carrier of R : Z * b1 = b1 * 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 () is Element of bool the carrier of R
the carrier of () is non empty set
Z |^ (carr ()) 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 ()) is Element of bool the carrier of R
{ (b1 |^ b2) where b1, b2 is Element of the carrier of R : ( b1 in K462( the carrier of R,Z) & b2 in carr () ) } 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 () is Element of bool the carrier of R
the carrier of () is non empty set
Z |^ (carr ()) 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 ()) is Element of bool the carrier of R
{ (b1 |^ b2) where b1, b2 is Element of the carrier of R : ( b1 in K462( the carrier of R,Z) & b2 in carr () ) } is set
[: the carrier of R,():] is non empty set
bool [: the carrier of R,():] 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<