REAL is non empty V33() V167() V168() V169() V173() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V33() V38() V39() V167() V168() V169() V170() V171() V172() V173() Element of bool REAL
bool REAL is V33() set
INT is non empty V33() V167() V168() V169() V170() V171() V173() set
COMPLEX is non empty V33() V167() V173() set
RAT is non empty V33() V167() V168() V169() V170() V173() set
[:COMPLEX,COMPLEX:] is V33() complex-yielding set
bool [:COMPLEX,COMPLEX:] is V33() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is V33() complex-yielding set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is V33() set
[:REAL,REAL:] is V33() complex-yielding V158() V159() set
bool [:REAL,REAL:] is V33() set
[:[:REAL,REAL:],REAL:] is V33() complex-yielding V158() V159() set
bool [:[:REAL,REAL:],REAL:] is V33() set
[:RAT,RAT:] is RAT -valued V33() complex-yielding V158() V159() set
bool [:RAT,RAT:] is V33() set
[:[:RAT,RAT:],RAT:] is RAT -valued V33() complex-yielding V158() V159() set
bool [:[:RAT,RAT:],RAT:] is V33() set
[:INT,INT:] is RAT -valued INT -valued V33() complex-yielding V158() V159() set
bool [:INT,INT:] is V33() set
[:[:INT,INT:],INT:] is RAT -valued INT -valued V33() complex-yielding V158() V159() set
bool [:[:INT,INT:],INT:] is V33() set
[:NAT,NAT:] is RAT -valued INT -valued V33() complex-yielding V158() V159() V160() set
[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued V33() complex-yielding V158() V159() V160() set
bool [:[:NAT,NAT:],NAT:] is V33() set
omega is non empty epsilon-transitive epsilon-connected ordinal V33() V38() V39() V167() V168() V169() V170() V171() V172() V173() set
bool omega is V33() set
bool NAT is V33() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real positive non negative V167() V168() V169() V170() V171() V172() Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real positive non negative V167() V168() V169() V170() V171() V172() Element of NAT
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural functional V33() V38() V40( {} ) FinSequence-membered ext-real non positive non negative V167() V168() V169() V170() V171() V172() V173() set
F_Real is non empty non degenerated non trivial V71() V91() V94() V114() V116() V118() V121() V122() V123() right-distributive left-distributive right_unital well-unital V135() left_unital L11()
the carrier of F_Real is non empty non trivial V167() V168() V169() set
the carrier of F_Real * is non empty functional FinSequence-membered FinSequenceSet of the carrier of F_Real
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real positive non negative V167() V168() V169() V170() V171() V172() Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real functional V30() V31() V33() V38() V40( {} ) FinSequence-membered ext-real non positive non negative V167() V168() V169() V170() V171() V172() V173() Element of NAT
[:NAT,REAL:] is V33() complex-yielding V158() V159() set
bool [:NAT,REAL:] is V33() set
addreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like V27([:REAL,REAL:], REAL ) complex-yielding V158() V159() Element of bool [:[:REAL,REAL:],REAL:]
multreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like V27([:REAL,REAL:], REAL ) complex-yielding V158() V159() Element of bool [:[:REAL,REAL:],REAL:]
G11(REAL,addreal,multreal,1,0) is V94() L11()
Seg 1 is non empty trivial V33() V40(1) V167() V168() V169() V170() V171() V172() Element of bool NAT
{1} is non empty trivial V40(1) V167() V168() V169() V170() V171() V172() set
Seg 2 is non empty V33() V40(2) V167() V168() V169() V170() V171() V172() Element of bool NAT
{1,2} is non empty V167() V168() V169() V170() V171() V172() set
<*> REAL is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like NAT -defined REAL -valued Function-like functional V33() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-yielding V158() V159() V160() V167() V168() V169() V170() V171() V172() V173() FinSequence of REAL
Sum (<*> REAL) is V11() real ext-real Element of REAL
P1 is set
P1 * is non empty functional FinSequence-membered FinSequenceSet of P1
P2 is Relation-like NAT -defined P1 * -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1 *
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
P2 . n2 is FinSequence-like set
dom P2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
rng P2 is set
dom P2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
<*> P1 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like NAT -defined P1 -valued Function-like functional V33() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-yielding V158() V159() V160() V167() V168() V169() V170() V171() V172() V173() FinSequence of P1
dom P2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
P1 is real set
<*P1*> is non empty trivial Relation-like NAT -defined Function-like one-to-one V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V158() V159() V161() V162() V163() V164() set
<*P1*> is non empty trivial Relation-like NAT -defined Function-like one-to-one V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V158() V159() V161() V162() V163() V164() set
rng <*P1*> is V167() V168() V169() Element of bool REAL
P1 is non empty set
P2 is Element of P1
n2 is non empty epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real positive non negative set
n2 |-> P2 is Relation-like NAT -defined P1 -valued Function-like V33() V40(n2) FinSequence-like FinSubsequence-like Element of n2 -tuples_on P1
n2 -tuples_on P1 is non empty functional FinSequence-membered FinSequenceSet of P1
P1 * is non empty functional FinSequence-membered FinSequenceSet of P1
{ b1 where b1 is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like Element of P1 * : len b1 = n2 } is set
Seg n2 is non empty V33() V40(n2) V167() V168() V169() V170() V171() V172() Element of bool NAT
(Seg n2) --> P2 is Relation-like Seg n2 -defined {P2} -valued Function-like V27( Seg n2,{P2}) V33() FinSequence-like FinSubsequence-like Element of bool [:(Seg n2),{P2}:]
{P2} is non empty trivial V40(1) set
[:(Seg n2),{P2}:] is set
bool [:(Seg n2),{P2}:] is set
m is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
len m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
dom m is V167() V168() V169() V170() V171() V172() Element of bool NAT
dom (n2 |-> P2) is V40(n2) V167() V168() V169() V170() V171() V172() Element of bool NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
m . n1 is set
(n2 |-> P2) . n1 is set
n1 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
m . n1 is set
P1 is non empty set
P2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg P2 is V33() V40(P2) V167() V168() V169() V170() V171() V172() Element of bool NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
Seg n2 is V33() V40(n2) V167() V168() V169() V170() V171() V172() Element of bool NAT
m is Element of P1
n1 is Element of P1
P is Relation-like Function-like set
dom P is set
P is Relation-like Function-like set
dom P is set
i is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
rng i is set
p is set
dom i is V167() V168() V169() V170() V171() V172() Element of bool NAT
p1 is set
i . p1 is set
p is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
len p is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
p1 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
p . p1 is set
P1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
dom P1 is V167() V168() V169() V170() V171() V172() Element of bool NAT
len P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P2 is Relation-like NAT -defined REAL -valued Function-like V27( NAT , REAL ) complex-yielding V158() V159() Element of bool [:NAT,REAL:]
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
P2 . n2 is V11() real ext-real Element of REAL
n2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real positive non negative V167() V168() V169() V170() V171() V172() Element of NAT
P2 . (n2 + 1) is V11() real ext-real Element of REAL
P1 . (n2 + 1) is V11() real ext-real Element of REAL
(P2 . n2) + (P1 . (n2 + 1)) is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
P2 . n2 is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P2 . m is V11() real ext-real Element of REAL
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real positive non negative V167() V168() V169() V170() V171() V172() Element of NAT
P2 . (m + 1) is V11() real ext-real Element of REAL
P2 . m is V11() real ext-real Element of REAL
P2 . (m + 1) is V11() real ext-real Element of REAL
P2 . (m + 1) is V11() real ext-real Element of REAL
P2 . (m + 1) is V11() real ext-real Element of REAL
P2 . (m + 1) is V11() real ext-real Element of REAL
P2 . 0 is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
P2 . m is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
m is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
P2 . n2 is V11() real ext-real Element of REAL
P2 . m is V11() real ext-real Element of REAL
P1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
dom P1 is V167() V168() V169() V170() V171() V172() Element of bool NAT
P1 . 1 is V11() real ext-real Element of REAL
P2 is Relation-like NAT -defined REAL -valued Function-like V27( NAT , REAL ) complex-yielding V158() V159() Element of bool [:NAT,REAL:]
P2 . 1 is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
P1 . n2 is V11() real ext-real Element of REAL
P2 . n2 is V11() real ext-real Element of REAL
n2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real positive non negative V167() V168() V169() V170() V171() V172() Element of NAT
P1 . (n2 + 1) is V11() real ext-real Element of REAL
P2 . (n2 + 1) is V11() real ext-real Element of REAL
P1 . (n2 + 1) is V11() real ext-real Element of REAL
(P2 . n2) + (P1 . (n2 + 1)) is V11() real ext-real Element of REAL
P2 . (n2 + 1) is V11() real ext-real Element of REAL
P1 . (n2 + 1) is V11() real ext-real Element of REAL
P2 . (n2 + 1) is V11() real ext-real Element of REAL
P1 . (n2 + 1) is V11() real ext-real Element of REAL
P2 . (n2 + 1) is V11() real ext-real Element of REAL
P2 . (n2 + 1) is V11() real ext-real Element of REAL
P1 . 0 is V11() real ext-real Element of REAL
P2 . 0 is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
P1 . n2 is V11() real ext-real Element of REAL
P2 . n2 is V11() real ext-real Element of REAL
P1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
dom P1 is V167() V168() V169() V170() V171() V172() Element of bool NAT
Sum P1 is V11() real ext-real Element of REAL
len P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
P1 . P2 is V11() real ext-real Element of REAL
len P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
P1 . P2 is V11() real ext-real Element of REAL
P1 . 1 is V11() real ext-real Element of REAL
m is Relation-like NAT -defined REAL -valued Function-like V27( NAT , REAL ) complex-yielding V158() V159() Element of bool [:NAT,REAL:]
m . 1 is V11() real ext-real Element of REAL
m . (len P1) is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P1 . n2 is V11() real ext-real Element of REAL
m . n2 is V11() real ext-real Element of REAL
len P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P1 is V11() real ext-real Element of REAL
P2 is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
m is Relation-like NAT -defined REAL -valued Function-like V27( NAT , REAL ) complex-yielding V158() V159() Element of bool [:NAT,REAL:]
n1 is set
P is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m . P is V11() real ext-real Element of REAL
P is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m . P is V11() real ext-real Element of REAL
P is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m . P is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m . i is V11() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m . p is V11() real ext-real Element of REAL
p1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m . p1 is V11() real ext-real Element of REAL
n1 is Relation-like Function-like set
dom n1 is set
P is set
n1 . P is set
i is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m . i is V11() real ext-real Element of REAL
P is Relation-like NAT -defined REAL -valued Function-like V27( NAT , REAL ) complex-yielding V158() V159() Element of bool [:NAT,REAL:]
i is Relation-like NAT -defined REAL -valued Function-like V27( NAT , REAL ) complex-yielding V158() V159() Element of bool [:NAT,REAL:]
p is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
i . p is V11() real ext-real Element of REAL
m . p is V11() real ext-real Element of REAL
p1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
i . p1 is V11() real ext-real Element of REAL
e3 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m . e3 is V11() real ext-real Element of REAL
n1 is Relation-like NAT -defined REAL -valued Function-like V27( NAT , REAL ) complex-yielding V158() V159() Element of bool [:NAT,REAL:]
n1 is Relation-like NAT -defined REAL -valued Function-like V27( NAT , REAL ) complex-yielding V158() V159() Element of bool [:NAT,REAL:]
n1 . 0 is V11() real ext-real Element of REAL
P is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
n1 . P is V11() real ext-real Element of REAL
m . P is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
n1 . i is V11() real ext-real Element of REAL
P1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Sum P1 is V11() real ext-real Element of REAL
NAT --> 0 is T-Sequence-like Relation-like NAT -defined REAL -valued INT -valued RAT -valued Function-like V27( NAT , REAL ) complex-yielding V158() V159() V160() Element of bool [:NAT,REAL:]
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
n2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real positive non negative V167() V168() V169() V170() V171() V172() Element of NAT
(NAT --> 0) . (n2 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative Element of REAL
(NAT --> 0) . n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative Element of REAL
P1 . (n2 + 1) is V11() real ext-real Element of REAL
((NAT --> 0) . n2) + (P1 . (n2 + 1)) is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
(NAT --> 0) . n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative Element of REAL
(NAT --> 0) . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative Element of REAL
(NAT --> 0) . (len P1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative Element of REAL
P1 . 1 is V11() real ext-real Element of REAL
P2 is Relation-like NAT -defined REAL -valued Function-like V27( NAT , REAL ) complex-yielding V158() V159() Element of bool [:NAT,REAL:]
P2 . 1 is V11() real ext-real Element of REAL
P2 . (len P1) is V11() real ext-real Element of REAL
n2 is Relation-like NAT -defined REAL -valued Function-like V27( NAT , REAL ) complex-yielding V158() V159() Element of bool [:NAT,REAL:]
n2 . 0 is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real positive non negative V167() V168() V169() V170() V171() V172() Element of NAT
n2 . (m + 1) is V11() real ext-real Element of REAL
n2 . m is V11() real ext-real Element of REAL
P1 . (m + 1) is V11() real ext-real Element of REAL
(n2 . m) + (P1 . (m + 1)) is V11() real ext-real Element of REAL
P2 . (m + 1) is V11() real ext-real Element of REAL
P2 . m is V11() real ext-real Element of REAL
(P2 . m) + (P1 . (m + 1)) is V11() real ext-real Element of REAL
n2 . (len P1) is V11() real ext-real Element of REAL
P1 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
P2 is set
P2 * is non empty functional FinSequence-membered FinSequenceSet of P2
n2 is Relation-like NAT -defined P2 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P2
P1 |-> n2 is Relation-like NAT -defined Function-like V33() V40(P1) FinSequence-like FinSubsequence-like set
Seg P1 is V33() V40(P1) V167() V168() V169() V170() V171() V172() Element of bool NAT
(Seg P1) --> n2 is Relation-like Seg P1 -defined {n2} -valued Function-like V27( Seg P1,{n2}) V33() FinSequence-like FinSubsequence-like Element of bool [:(Seg P1),{n2}:]
{n2} is non empty trivial V40(1) set
[:(Seg P1),{n2}:] is set
bool [:(Seg P1),{n2}:] is set
P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg P1 is V33() V40(P1) V167() V168() V169() V170() V171() V172() Element of bool NAT
P2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
Seg P2 is V33() V40(P2) V167() V168() V169() V170() V171() V172() Element of bool NAT
n2 is set
n2 * is non empty functional FinSequence-membered FinSequenceSet of n2
m is Relation-like NAT -defined n2 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of n2
n1 is Relation-like NAT -defined n2 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of n2
P1 is set
P1 * is non empty functional FinSequence-membered FinSequenceSet of P1
P2 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
dom P2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
n2 is Relation-like NAT -defined P1 * -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1 *
rng n2 is set
m is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
dom n2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(P1,n2,n1) is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
P is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len P is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
[:NAT,P1:] is set
bool [:NAT,P1:] is set
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P2 . P is set
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
rng P2 is set
m is set
n1 is set
P2 . n1 is set
P is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
len P is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
len P is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m is set
m is set
P1 is set
P1 * is non empty functional FinSequence-membered FinSequenceSet of P1
P2 is Relation-like NAT -defined P1 * -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1 *
dom P2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(P1,P2,m) is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
len (P1,P2,m) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(P1,P2,m) is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
len (P1,P2,m) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
n1 is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
len n1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
[P1,P2] is set
{P1,P2} is non empty V167() V168() V169() V170() V171() V172() set
{P1} is non empty trivial V40(1) V167() V168() V169() V170() V171() V172() set
{{P1,P2},{P1}} is non empty set
n2 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like tabular set
Indices n2 is set
len n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len n2) is V33() V40( len n2) V167() V168() V169() V170() V171() V172() Element of bool NAT
width n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (width n2) is V33() V40( width n2) V167() V168() V169() V170() V171() V172() Element of bool NAT
dom n2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
[:(dom n2),(Seg (width n2)):] is INT -valued RAT -valued complex-yielding V158() V159() V160() set
P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
[P1,P2] is set
{P1,P2} is non empty V167() V168() V169() V170() V171() V172() set
{P1} is non empty trivial V40(1) V167() V168() V169() V170() V171() V172() set
{{P1,P2},{P1}} is non empty set
n2 is non empty set
n2 * is non empty functional FinSequence-membered FinSequenceSet of n2
m is Relation-like NAT -defined n2 * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of n2 *
Indices m is set
dom m is V167() V168() V169() V170() V171() V172() Element of bool NAT
(n2,m,P1) is Relation-like NAT -defined n2 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of n2
dom (n2,m,P1) is V167() V168() V169() V170() V171() V172() Element of bool NAT
width m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (width m) is V33() V40( width m) V167() V168() V169() V170() V171() V172() Element of bool NAT
len m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len m) is V33() V40( len m) V167() V168() V169() V170() V171() V172() Element of bool NAT
len (n2,m,P1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len (n2,m,P1)) is V33() V40( len (n2,m,P1)) V167() V168() V169() V170() V171() V172() Element of bool NAT
P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
[P1,P2] is set
{P1,P2} is non empty V167() V168() V169() V170() V171() V172() set
{P1} is non empty trivial V40(1) V167() V168() V169() V170() V171() V172() set
{{P1,P2},{P1}} is non empty set
n2 is non empty set
n2 * is non empty functional FinSequence-membered FinSequenceSet of n2
m is Relation-like NAT -defined n2 * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of n2 *
Indices m is set
m * (P1,P2) is Element of n2
(n2,m,P1) is Relation-like NAT -defined n2 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of n2
(n2,m,P1) . P2 is set
n1 is Relation-like NAT -defined n2 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of n2
n1 . P2 is set
P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
[P1,P2] is set
{P1,P2} is non empty V167() V168() V169() V170() V171() V172() set
{P1} is non empty trivial V40(1) V167() V168() V169() V170() V171() V172() set
{{P1,P2},{P1}} is non empty set
n2 is non empty set
n2 * is non empty functional FinSequence-membered FinSequenceSet of n2
m is Relation-like NAT -defined n2 * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of n2 *
Indices m is set
Col (m,P2) is Relation-like NAT -defined n2 -valued Function-like V33() V40( len m) FinSequence-like FinSubsequence-like Element of (len m) -tuples_on n2
len m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(len m) -tuples_on n2 is non empty functional FinSequence-membered FinSequenceSet of n2
{ b1 where b1 is Relation-like NAT -defined n2 -valued Function-like V33() FinSequence-like FinSubsequence-like Element of n2 * : len b1 = len m } is set
dom (Col (m,P2)) is V40( len m) V167() V168() V169() V170() V171() V172() Element of bool NAT
Line (m,P1) is Relation-like NAT -defined n2 -valued Function-like V33() V40( width m) FinSequence-like FinSubsequence-like Element of (width m) -tuples_on n2
width m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(width m) -tuples_on n2 is non empty functional FinSequence-membered FinSequenceSet of n2
{ b1 where b1 is Relation-like NAT -defined n2 -valued Function-like V33() FinSequence-like FinSubsequence-like Element of n2 * : len b1 = width m } is set
dom (Line (m,P1)) is V40( width m) V167() V168() V169() V170() V171() V172() Element of bool NAT
dom m is V167() V168() V169() V170() V171() V172() Element of bool NAT
Seg (len m) is V33() V40( len m) V167() V168() V169() V170() V171() V172() Element of bool NAT
len (Col (m,P2)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len (Col (m,P2))) is V33() V40( len (Col (m,P2))) V167() V168() V169() V170() V171() V172() Element of bool NAT
(n2,m,P1) is Relation-like NAT -defined n2 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of n2
dom (n2,m,P1) is V167() V168() V169() V170() V171() V172() Element of bool NAT
P1 is non empty set
P1 * is non empty functional FinSequence-membered FinSequenceSet of P1
P2 is non empty set
P2 * is non empty functional FinSequence-membered FinSequenceSet of P2
n2 is Relation-like NAT -defined P1 * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of P1 *
dom n2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
m is Relation-like NAT -defined P2 * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of P2 *
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Line (n2,n1) is Relation-like NAT -defined P1 -valued Function-like V33() V40( width n2) FinSequence-like FinSubsequence-like Element of (width n2) -tuples_on P1
width n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(width n2) -tuples_on P1 is non empty functional FinSequence-membered FinSequenceSet of P1
{ b1 where b1 is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like Element of P1 * : len b1 = width n2 } is set
(P1,n2,n1) is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
Line (m,n1) is Relation-like NAT -defined P2 -valued Function-like V33() V40( width m) FinSequence-like FinSubsequence-like Element of (width m) -tuples_on P2
width m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(width m) -tuples_on P2 is non empty functional FinSequence-membered FinSequenceSet of P2
{ b1 where b1 is Relation-like NAT -defined P2 -valued Function-like V33() FinSequence-like FinSubsequence-like Element of P2 * : len b1 = width m } is set
P1 is non empty set
P1 * is non empty functional FinSequence-membered FinSequenceSet of P1
P2 is non empty set
P2 * is non empty functional FinSequence-membered FinSequenceSet of P2
n2 is Relation-like NAT -defined P1 * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of P1 *
width n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (width n2) is V33() V40( width n2) V167() V168() V169() V170() V171() V172() Element of bool NAT
m is Relation-like NAT -defined P2 * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of P2 *
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Col (n2,n1) is Relation-like NAT -defined P1 -valued Function-like V33() V40( len n2) FinSequence-like FinSubsequence-like Element of (len n2) -tuples_on P1
len n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(len n2) -tuples_on P1 is non empty functional FinSequence-membered FinSequenceSet of P1
{ b1 where b1 is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like Element of P1 * : len b1 = len n2 } is set
dom (Col (n2,n1)) is V40( len n2) V167() V168() V169() V170() V171() V172() Element of bool NAT
Col (m,n1) is Relation-like NAT -defined P2 -valued Function-like V33() V40( len m) FinSequence-like FinSubsequence-like Element of (len m) -tuples_on P2
len m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(len m) -tuples_on P2 is non empty functional FinSequence-membered FinSequenceSet of P2
{ b1 where b1 is Relation-like NAT -defined P2 -valued Function-like V33() FinSequence-like FinSubsequence-like Element of P2 * : len b1 = len m } is set
P is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
(Col (n2,n1)) . P is set
(Col (m,n1)) . P is set
len (Col (n2,n1)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len (Col (n2,n1))) is V33() V40( len (Col (n2,n1))) V167() V168() V169() V170() V171() V172() Element of bool NAT
Seg (len n2) is V33() V40( len n2) V167() V168() V169() V170() V171() V172() Element of bool NAT
[P,n1] is set
{P,n1} is non empty V167() V168() V169() V170() V171() V172() set
{P} is non empty trivial V40(1) V167() V168() V169() V170() V171() V172() set
{{P,n1},{P}} is non empty set
Indices n2 is set
dom n2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
n2 * (P,n1) is Element of P1
m * (P,n1) is Element of P2
len (Col (n2,n1)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len (Col (n2,n1))) is V33() V40( len (Col (n2,n1))) V167() V168() V169() V170() V171() V172() Element of bool NAT
Seg (len n2) is V33() V40( len n2) V167() V168() V169() V170() V171() V172() Element of bool NAT
len (Col (m,n1)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len (Col (m,n1))) is V33() V40( len (Col (m,n1))) V167() V168() V169() V170() V171() V172() Element of bool NAT
dom (Col (m,n1)) is V40( len m) V167() V168() V169() V170() V171() V172() Element of bool NAT
P1 is non empty set
P1 * is non empty functional FinSequence-membered FinSequenceSet of P1
P2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
m is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
len m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
n2 |-> m is Relation-like NAT -defined Function-like V33() V40(n2) FinSequence-like FinSubsequence-like set
Seg n2 is V33() V40(n2) V167() V168() V169() V170() V171() V172() Element of bool NAT
(Seg n2) --> m is Relation-like Seg n2 -defined {m} -valued Function-like V27( Seg n2,{m}) V33() FinSequence-like FinSubsequence-like Element of bool [:(Seg n2),{m}:]
{m} is non empty trivial V40(1) set
[:(Seg n2),{m}:] is set
bool [:(Seg n2),{m}:] is set
n1 is Relation-like NAT -defined P1 * -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1 *
len n1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
dom n1 is V167() V168() V169() V170() V171() V172() Element of bool NAT
P is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(P1,n1,P) is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
len (P1,n1,P) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P is Relation-like NAT -defined P1 * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of P1 *
rng P is set
i is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
len i is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
dom P is V167() V168() V169() V170() V171() V172() Element of bool NAT
p is set
P . p is FinSequence-like set
P1 is non empty set
P1 * is non empty functional FinSequence-membered FinSequenceSet of P1
P2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg P2 is V33() V40(P2) V167() V168() V169() V170() V171() V172() Element of bool NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
m is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
Seg m is V33() V40(m) V167() V168() V169() V170() V171() V172() Element of bool NAT
n1 is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
len n1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
len P is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
i is Relation-like NAT -defined P1 * -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1 *
len i is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
dom i is V167() V168() V169() V170() V171() V172() Element of bool NAT
p is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(P1,i,p) is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
len (P1,i,p) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
p is Relation-like NAT -defined P1 * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of P1 *
rng p is set
p1 is Relation-like NAT -defined P1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of P1
len p1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
dom p is V167() V168() V169() V170() V171() V172() Element of bool NAT
e3 is set
p . e3 is FinSequence-like set
P1 is V11() real ext-real Element of REAL
P2 is Relation-like NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of REAL *
Indices P2 is set
dom P2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(REAL,P2,n2) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
dom (REAL,P2,n2) is V167() V168() V169() V170() V171() V172() Element of bool NAT
[n2,m] is set
{n2,m} is non empty V167() V168() V169() V170() V171() V172() set
{n2} is non empty trivial V40(1) V167() V168() V169() V170() V171() V172() set
{{n2,m},{n2}} is non empty set
P2 * (n2,m) is V11() real ext-real Element of REAL
(REAL,P2,n2) . m is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
[n2,m] is set
{n2,m} is non empty V167() V168() V169() V170() V171() V172() set
{n2} is non empty trivial V40(1) V167() V168() V169() V170() V171() V172() set
{{n2,m},{n2}} is non empty set
(REAL,P2,n2) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
dom (REAL,P2,n2) is V167() V168() V169() V170() V171() V172() Element of bool NAT
(REAL,P2,n2) . m is V11() real ext-real Element of REAL
P2 * (n2,m) is V11() real ext-real Element of REAL
P1 is V11() real ext-real Element of REAL
P2 is Relation-like NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of REAL *
Indices P2 is set
dom P2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Line (P2,n2) is Relation-like NAT -defined REAL -valued Function-like V33() V40( width P2) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of (width P2) -tuples_on REAL
width P2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(width P2) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = width P2 } is set
dom (Line (P2,n2)) is V40( width P2) V167() V168() V169() V170() V171() V172() Element of bool NAT
(REAL,P2,n2) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
(Line (P2,n2)) . m is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(REAL,P2,n2) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
Line (P2,n2) is Relation-like NAT -defined REAL -valued Function-like V33() V40( width P2) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of (width P2) -tuples_on REAL
dom (REAL,P2,n2) is V167() V168() V169() V170() V171() V172() Element of bool NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(REAL,P2,n2) . m is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(REAL,P2,n2) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
dom (REAL,P2,n2) is V167() V168() V169() V170() V171() V172() Element of bool NAT
(REAL,P2,n2) . m is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
[n2,m] is set
{n2,m} is non empty V167() V168() V169() V170() V171() V172() set
{n2} is non empty trivial V40(1) V167() V168() V169() V170() V171() V172() set
{{n2,m},{n2}} is non empty set
P2 * (n2,m) is V11() real ext-real Element of REAL
P1 is V11() real ext-real Element of REAL
P2 is Relation-like NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of REAL *
Indices P2 is set
width P2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (width P2) is V33() V40( width P2) V167() V168() V169() V170() V171() V172() Element of bool NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Col (P2,m) is Relation-like NAT -defined REAL -valued Function-like V33() V40( len P2) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of (len P2) -tuples_on REAL
len P2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(len P2) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = len P2 } is set
dom (Col (P2,m)) is V40( len P2) V167() V168() V169() V170() V171() V172() Element of bool NAT
Line (P2,n2) is Relation-like NAT -defined REAL -valued Function-like V33() V40( width P2) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of (width P2) -tuples_on REAL
(width P2) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = width P2 } is set
len (Line (P2,n2)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len (Line (P2,n2))) is V33() V40( len (Line (P2,n2))) V167() V168() V169() V170() V171() V172() Element of bool NAT
dom (Line (P2,n2)) is V40( width P2) V167() V168() V169() V170() V171() V172() Element of bool NAT
[n2,m] is set
{n2,m} is non empty V167() V168() V169() V170() V171() V172() set
{n2} is non empty trivial V40(1) V167() V168() V169() V170() V171() V172() set
{{n2,m},{n2}} is non empty set
dom P2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
(Line (P2,n2)) . m is V11() real ext-real Element of REAL
(Col (P2,m)) . n2 is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Line (P2,n2) is Relation-like NAT -defined REAL -valued Function-like V33() V40( width P2) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of (width P2) -tuples_on REAL
dom (Line (P2,n2)) is V40( width P2) V167() V168() V169() V170() V171() V172() Element of bool NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(Line (P2,n2)) . m is V11() real ext-real Element of REAL
len (Line (P2,n2)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len (Line (P2,n2))) is V33() V40( len (Line (P2,n2))) V167() V168() V169() V170() V171() V172() Element of bool NAT
Seg (len P2) is V33() V40( len P2) V167() V168() V169() V170() V171() V172() Element of bool NAT
Col (P2,m) is Relation-like NAT -defined REAL -valued Function-like V33() V40( len P2) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of (len P2) -tuples_on REAL
len (Col (P2,m)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len (Col (P2,m))) is V33() V40( len (Col (P2,m))) V167() V168() V169() V170() V171() V172() Element of bool NAT
dom (Col (P2,m)) is V40( len P2) V167() V168() V169() V170() V171() V172() Element of bool NAT
(Col (P2,m)) . n2 is V11() real ext-real Element of REAL
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
[n2,m] is set
{n2,m} is non empty V167() V168() V169() V170() V171() V172() set
{n2} is non empty trivial V40(1) V167() V168() V169() V170() V171() V172() set
{{n2,m},{n2}} is non empty set
P2 * (n2,m) is V11() real ext-real Element of REAL
P1 is Relation-like NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of REAL *
len P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P2 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len P2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
dom P2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P2 . n2 is V11() real ext-real Element of REAL
(REAL,P1,n2) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
Sum (REAL,P1,n2) is V11() real ext-real Element of REAL
P2 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len P2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
dom P2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
n2 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
dom n2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
Seg (len P1) is V33() V40( len P1) V167() V168() V169() V170() V171() V172() Element of bool NAT
m is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
P2 . m is V11() real ext-real Element of REAL
n2 . m is V11() real ext-real Element of REAL
(REAL,P1,m) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
Sum (REAL,P1,m) is V11() real ext-real Element of REAL
P1 is Relation-like NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of REAL *
(P1) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len (P1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
len P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len P1) is V33() V40( len P1) V167() V168() V169() V170() V171() V172() Element of bool NAT
P2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(P1) . P2 is V11() real ext-real Element of REAL
Line (P1,P2) is Relation-like NAT -defined REAL -valued Function-like V33() V40( width P1) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of (width P1) -tuples_on REAL
width P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(width P1) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = width P1 } is set
Sum (Line (P1,P2)) is V11() real ext-real Element of REAL
dom P1 is V167() V168() V169() V170() V171() V172() Element of bool NAT
Seg (len (P1)) is V33() V40( len (P1)) V167() V168() V169() V170() V171() V172() Element of bool NAT
dom (P1) is V167() V168() V169() V170() V171() V172() Element of bool NAT
(REAL,P1,P2) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
Sum (REAL,P1,P2) is V11() real ext-real Element of REAL
P1 is Relation-like NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of REAL *
width P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
Seg (width P1) is V33() V40( width P1) V167() V168() V169() V170() V171() V172() Element of bool NAT
P2 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len P2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
dom P2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
P2 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len P2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
n2 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len n2 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
dom P2 is V167() V168() V169() V170() V171() V172() Element of bool NAT
m is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
P2 . m is V11() real ext-real Element of REAL
n2 . m is V11() real ext-real Element of REAL
Col (P1,m) is Relation-like NAT -defined REAL -valued Function-like V33() V40( len P1) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of (len P1) -tuples_on REAL
len P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(len P1) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = len P1 } is set
Sum (Col (P1,m)) is V11() real ext-real Element of REAL
P1 is Relation-like NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of REAL *
width P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(P1) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
P1 @ is Relation-like NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of REAL *
((P1 @)) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
width (P1 @) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
len (P1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
len ((P1 @)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
P2 is epsilon-transitive epsilon-connected ordinal natural V33() V38() ext-real non negative set
Seg (len (P1)) is V33() V40( len (P1)) V167() V168() V169() V170() V171() V172() Element of bool NAT
Seg (len P1) is V33() V40( len P1) V167() V168() V169() V170() V171() V172() Element of bool NAT
dom P1 is V167() V168() V169() V170() V171() V172() Element of bool NAT
Seg (width (P1 @)) is V33() V40( width (P1 @)) V167() V168() V169() V170() V171() V172() Element of bool NAT
((P1 @)) . P2 is V11() real ext-real Element of REAL
Col ((P1 @),P2) is Relation-like NAT -defined REAL -valued Function-like V33() V40( len (P1 @)) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of (len (P1 @)) -tuples_on REAL
len (P1 @) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
(len (P1 @)) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = len (P1 @) } is set
Sum (Col ((P1 @),P2)) is V11() real ext-real Element of REAL
Line (P1,P2) is Relation-like NAT -defined REAL -valued Function-like V33() V40( width P1) FinSequence-like FinSubsequence-like complex-yielding V158() V159() Element of (width P1) -tuples_on REAL
(width P1) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = width P1 } is set
Sum (Line (P1,P2)) is V11() real ext-real Element of REAL
(P1) . P2 is V11() real ext-real Element of REAL
P1 is Relation-like NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of REAL *
(P1) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
P1 @ is Relation-like NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() FinSequence of REAL *
((P1 @)) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() FinSequence of REAL
len (P1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
width P1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38() ext-real non negative V167() V168() V169() V170() V171() V172() Element of NAT
len ((P1 @)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() V33() V38()