:: MATRPROB semantic presentation

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

{ b

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

{ b

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

{ b

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

{ b

(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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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