:: PRVECT_2 semantic presentation

REAL is non empty V30() V167() V168() V169() V173() set

bool REAL is V30() set

RAT is non empty V30() V167() V168() V169() V170() V173() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
{{},1} is non empty V167() V168() V169() V170() V171() V172() set
INT is non empty V30() V167() V168() V169() V170() V171() V173() set
omega is non empty epsilon-transitive epsilon-connected ordinal V30() V35() V36() countable denumerable V167() V168() V169() V170() V171() V172() V173() set
bool omega is V30() set
bool NAT is V30() set
COMPLEX is non empty V30() V167() V173() set

bool is V30() set

bool is V30() set

K411() is non empty set
[:K411(),K411():] is Relation-like set
[:[:K411(),K411():],K411():] is Relation-like set
bool [:[:K411(),K411():],K411():] is set

[:[:REAL,K411():],K411():] is Relation-like V30() set
bool [:[:REAL,K411():],K411():] is V30() set
K417() is RLSStruct
the carrier of K417() is set
bool the carrier of K417() is set
K421() is Element of bool the carrier of K417()
[:K421(),K421():] is Relation-like set

bool [:[:K421(),K421():],REAL:] is set

bool [:1,1:] is set

bool [:[:1,1:],1:] is set

bool [:[:1,1:],REAL:] is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT

bool [:[:2,2:],REAL:] is set

the carrier of () is non empty set

3 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
Seg 1 is non empty trivial V30() V37(1) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
- 1 is V42() real ext-real Element of REAL

seq is V42() real ext-real set
yy0 is V42() real ext-real set

G . j is V42() real ext-real Element of REAL
(G . j) - seq is V42() real ext-real Element of REAL
abs ((G . j) - seq) is V42() real ext-real Element of REAL
abs (abs ((G . j) - seq)) is V42() real ext-real Element of REAL
I . j is V42() real ext-real Element of REAL
(I . j) - 0 is V42() real ext-real Element of REAL
abs ((I . j) - 0) is V42() real ext-real Element of REAL

I . j is V42() real ext-real Element of REAL
(I . j) - 0 is V42() real ext-real Element of REAL
abs ((I . j) - 0) is V42() real ext-real Element of REAL
yy0 is V42() real ext-real set

I . j is V42() real ext-real Element of REAL
(I . j) - 0 is V42() real ext-real Element of REAL
abs ((I . j) - 0) is V42() real ext-real Element of REAL
G . j is V42() real ext-real Element of REAL
(G . j) - seq is V42() real ext-real Element of REAL
abs ((G . j) - seq) is V42() real ext-real Element of REAL
abs (abs ((G . j) - seq)) is V42() real ext-real Element of REAL

G . j is V42() real ext-real Element of REAL
(G . j) - seq is V42() real ext-real Element of REAL
abs ((G . j) - seq) is V42() real ext-real Element of REAL

Seg (len G) is V30() V37( len G) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
|.G.| is V42() real ext-real non negative Element of REAL

Sum (sqr G) is V42() real ext-real Element of REAL
sqrt (Sum (sqr G)) is V42() real ext-real Element of REAL
|.I.| is V42() real ext-real non negative Element of REAL

Sum (sqr I) is V42() real ext-real Element of REAL
sqrt (Sum (sqr I)) is V42() real ext-real Element of REAL

(sqr G) . seq is V42() real ext-real Element of REAL
(sqr I) . seq is V42() real ext-real Element of REAL
G . seq is V42() real ext-real Element of REAL
I . seq is V42() real ext-real Element of REAL
(G . seq) ^2 is V42() real ext-real Element of REAL
(G . seq) * (G . seq) is V42() real ext-real set
(I . seq) ^2 is V42() real ext-real Element of REAL
(I . seq) * (I . seq) is V42() real ext-real set

Seg (len (sqr I)) is V30() V37( len (sqr I)) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
dom (sqr I) is countable V167() V168() V169() V170() V171() V172() Element of bool NAT
dom I is countable V167() V168() V169() V170() V171() V172() Element of bool NAT

Seg (len (sqr G)) is V30() V37( len (sqr G)) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
dom (sqr G) is countable V167() V168() V169() V170() V171() V172() Element of bool NAT
dom G is countable V167() V168() V169() V170() V171() V172() Element of bool NAT

{ } is set

{ } is set

dom G is countable V167() V168() V169() V170() V171() V172() Element of bool NAT

{ } is set
Seg (len G) is V30() V37( len G) countable V167() V168() V169() V170() V171() V172() Element of bool NAT

is functional non empty trivial V37(1) with_common_domain V167() V168() V169() V170() V171() V172() set

bool [:(Seg (len G)),:] is set

{ } is set

yy0 . y0 is V42() real ext-real Element of REAL
len ((len G) |-> 0) is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
dom ((len G) |-> 0) is V37( len G) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
dom yy0 is V37( len G) countable V167() V168() V169() V170() V171() V172() Element of bool NAT

dom G is set
I is set

dom seq is set
yy0 is set
seq . yy0 is set
G . yy0 is set
[:I,(G . yy0):] is Relation-like set
[:[:I,(G . yy0):],(G . yy0):] is Relation-like set
bool [:[:I,(G . yy0):],(G . yy0):] is set
pr2 (I,(G . yy0)) is Relation-like Function-like quasi_total Element of bool [:[:I,(G . yy0):],(G . yy0):]

I is set
seq is Relation-like Function-like (G,I)
dom G is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT
dom seq is set
len G is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len G) is non empty V30() V37( len G) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
G is set

len I is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
dom I is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT

dom seq is countable V167() V168() V169() V170() V171() V172() Element of bool NAT
yy0 is set
seq . yy0 is set
I . yy0 is set
[:G,(I . yy0):] is Relation-like set
[:[:G,(I . yy0):],(I . yy0):] is Relation-like set
bool [:[:G,(I . yy0):],(I . yy0):] is set

I is set
dom G is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT

seq . yy0 is set
G . yy0 is non empty set
[:I,(G . yy0):] is Relation-like set
[:[:I,(G . yy0):],(G . yy0):] is Relation-like set
bool [:[:I,(G . yy0):],(G . yy0):] is set
G is non empty set

[:G,():] is Relation-like set
[:[:G,():],():] is Relation-like set
bool [:[:G,():],():] is set
dom I is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT
seq is Relation-like Function-like V14([:G,():]) quasi_total Element of bool [:[:G,():],():]
yy0 is Relation-like Function-like V14([:G,():]) quasi_total Element of bool [:[:G,():],():]
y0 is Element of G

seq . (y0,x0) is Relation-like NAT -defined Function-like I -compatible Element of product I
dom (seq . (y0,x0)) is set
yy0 . (y0,x0) is Relation-like NAT -defined Function-like I -compatible Element of product I
dom (yy0 . (y0,x0)) is set
j is set
(seq . (y0,x0)) . j is set
(yy0 . (y0,x0)) . j is set

I is non empty set

[:I,():] is Relation-like set
[:[:I,():],():] is Relation-like set
bool [:[:I,():],():] is set
dom G is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT

yy0 is Element of I

x0 is set

G . j is non empty set
(G,I,seq,j) is Relation-like Function-like V14([:I,(G . j):]) quasi_total Element of bool [:[:I,(G . j):],(G . j):]
[:I,(G . j):] is Relation-like set
[:[:I,(G . j):],(G . j):] is Relation-like set
bool [:[:I,(G . j):],(G . j):] is set
y0 . j is Element of G . j
(G,I,seq,j) . (yy0,(y0 . j)) is Element of G . j

dom x0 is set
j is set
x0 . j is set
G . j is set

G . i0 is non empty set
(G,I,seq,i0) is Relation-like Function-like V14([:I,(G . i0):]) quasi_total Element of bool [:[:I,(G . i0):],(G . i0):]
[:I,(G . i0):] is Relation-like set
[:[:I,(G . i0):],(G . i0):] is Relation-like set
bool [:[:I,(G . i0):],(G . i0):] is set
y0 . i0 is Element of G . i0
(G,I,seq,i0) . (yy0,(y0 . i0)) is Element of G . i0

j . i0 is Element of G . i0
G . i0 is non empty set
(G,I,seq,i0) is Relation-like Function-like V14([:I,(G . i0):]) quasi_total Element of bool [:[:I,(G . i0):],(G . i0):]
[:I,(G . i0):] is Relation-like set
[:[:I,(G . i0):],(G . i0):] is Relation-like set
bool [:[:I,(G . i0):],(G . i0):] is set
y0 . i0 is Element of G . i0
(G,I,seq,i0) . (yy0,(y0 . i0)) is Element of G . i0
x0 . i0 is set

G . seqi is non empty set
(G,I,seq,seqi) is Relation-like Function-like V14([:I,(G . seqi):]) quasi_total Element of bool [:[:I,(G . seqi):],(G . seqi):]
[:I,(G . seqi):] is Relation-like set
[:[:I,(G . seqi):],(G . seqi):] is Relation-like set
bool [:[:I,(G . seqi):],(G . seqi):] is set
y0 . seqi is Element of G . seqi
(G,I,seq,seqi) . (yy0,(y0 . seqi)) is Element of G . seqi
yy0 is Relation-like Function-like V14([:I,():]) quasi_total Element of bool [:[:I,():],():]
y0 is Relation-like Function-like V14([:I,():]) quasi_total Element of bool [:[:I,():],():]
x0 is Element of I

yy0 . (x0,j) is Relation-like NAT -defined Function-like G -compatible Element of product G

(yy0 . (x0,j)) . i0 is Element of G . i0
G . i0 is non empty set
(G,I,seq,i0) is Relation-like Function-like V14([:I,(G . i0):]) quasi_total Element of bool [:[:I,(G . i0):],(G . i0):]
[:I,(G . i0):] is Relation-like set
[:[:I,(G . i0):],(G . i0):] is Relation-like set
bool [:[:I,(G . i0):],(G . i0):] is set
j . i0 is Element of G . i0
(G,I,seq,i0) . (x0,(j . i0)) is Element of G . i0

(y0 . (x0,j)) . i0 is Element of G . i0

I is set
rng <**> is non empty trivial V37(1) set
{} is non empty trivial V37(1) set

dom G is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT

G . I is set
rng G is non empty set

len G is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
dom G is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT
Seg (len G) is non empty V30() V37( len G) countable V167() V168() V169() V170() V171() V172() Element of bool NAT

the carrier of (G,seq) is non empty set

dom I is countable V167() V168() V169() V170() V171() V172() Element of bool NAT
rng I is set
seq is set
I . seq is set

I . yy0 is set

the carrier of (G,y0) is non empty set

len seq is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT

seq . yy0 is set

the carrier of (G,yy0) is non empty set

seq . y0 is set

the carrier of (G,x0) is non empty set

len I is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT

len seq is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT

dom yy0 is countable V167() V168() V169() V170() V171() V172() Element of bool NAT
yy0 . x0 is set

the carrier of (G,j) is non empty set

y0 . x0 is set

Seg (len yy0) is V30() V37( len yy0) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
dom y0 is countable V167() V168() V169() V170() V171() V172() Element of bool NAT

Seg (len y0) is V30() V37( len y0) countable V167() V168() V169() V170() V171() V172() Element of bool NAT

dom (G) is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT

G . I is set
dom G is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT
len G is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len G) is non empty V30() V37( len G) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
len (G) is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len (G)) is non empty V30() V37( len (G)) countable V167() V168() V169() V170() V171() V172() Element of bool NAT

len (G) is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
dom (G) is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT

len I is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
len G is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
dom G is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT

I . seq is set

the addF of (G,seq) is Relation-like Function-like V14([: the carrier of (G,seq), the carrier of (G,seq):]) quasi_total Element of bool [:[: the carrier of (G,seq), the carrier of (G,seq):], the carrier of (G,seq):]
the carrier of (G,seq) is non empty set
[: the carrier of (G,seq), the carrier of (G,seq):] is Relation-like set
[:[: the carrier of (G,seq), the carrier of (G,seq):], the carrier of (G,seq):] is Relation-like set
bool [:[: the carrier of (G,seq), the carrier of (G,seq):], the carrier of (G,seq):] is set

the carrier of (G,yy0) is non empty set
(G) . yy0 is set
(G) . seq is non empty set
[:((G) . seq),((G) . seq):] is Relation-like set
[:[:((G) . seq),((G) . seq):],((G) . seq):] is Relation-like set
bool [:[:((G) . seq),((G) . seq):],((G) . seq):] is set

(G) . yy0 is non empty set
[:((G) . yy0),((G) . yy0):] is Relation-like set

the carrier of (G,yy0) is non empty set
[: the carrier of (G,yy0), the carrier of (G,yy0):] is Relation-like set
seq . yy0 is Relation-like Function-like V14([:((G) . yy0),((G) . yy0):]) quasi_total Element of bool [:[:((G) . yy0),((G) . yy0):],((G) . yy0):]
[:[:((G) . yy0),((G) . yy0):],((G) . yy0):] is Relation-like set
bool [:[:((G) . yy0),((G) . yy0):],((G) . yy0):] is set
the addF of (G,yy0) is Relation-like Function-like V14([: the carrier of (G,yy0), the carrier of (G,yy0):]) quasi_total Element of bool [:[: the carrier of (G,yy0), the carrier of (G,yy0):], the carrier of (G,yy0):]
[:[: the carrier of (G,yy0), the carrier of (G,yy0):], the carrier of (G,yy0):] is Relation-like set
bool [:[: the carrier of (G,yy0), the carrier of (G,yy0):], the carrier of (G,yy0):] is set

dom yy0 is countable V167() V168() V169() V170() V171() V172() Element of bool NAT
yy0 . x0 is set

the addF of (G,j) is Relation-like Function-like V14([: the carrier of (G,j), the carrier of (G,j):]) quasi_total Element of bool [:[: the carrier of (G,j), the carrier of (G,j):], the carrier of (G,j):]
the carrier of (G,j) is non empty set
[: the carrier of (G,j), the carrier of (G,j):] is Relation-like set
[:[: the carrier of (G,j), the carrier of (G,j):], the carrier of (G,j):] is Relation-like set
bool [:[: the carrier of (G,j), the carrier of (G,j):], the carrier of (G,j):] is set

y0 . x0 is set

Seg (len yy0) is V30() V37( len yy0) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
dom y0 is countable V167() V168() V169() V170() V171() V172() Element of bool NAT

Seg (len y0) is V30() V37( len y0) countable V167() V168() V169() V170() V171() V172() Element of bool NAT

len I is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
len G is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
dom G is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT

I . seq is set

comp (G,seq) is Relation-like Function-like non empty V14( the carrier of (G,seq)) quasi_total Element of bool [: the carrier of (G,seq), the carrier of (G,seq):]
the carrier of (G,seq) is non empty set
[: the carrier of (G,seq), the carrier of (G,seq):] is Relation-like set
bool [: the carrier of (G,seq), the carrier of (G,seq):] is set

the carrier of (G,yy0) is non empty set
(G) . yy0 is set
(G) . seq is non empty set
[:((G) . seq),((G) . seq):] is Relation-like set
bool [:((G) . seq),((G) . seq):] is set

(G) . yy0 is non empty set

the carrier of (G,yy0) is non empty set
seq . yy0 is Relation-like Function-like non empty V14((G) . yy0) quasi_total Element of bool [:((G) . yy0),((G) . yy0):]
[:((G) . yy0),((G) . yy0):] is Relation-like set
bool [:((G) . yy0),((G) . yy0):] is set
comp (G,yy0) is Relation-like Function-like non empty V14( the carrier of (G,yy0)) quasi_total Element of bool [: the carrier of (G,yy0), the carrier of (G,yy0):]
[: the carrier of (G,yy0), the carrier of (G,yy0):] is Relation-like set
bool [: the carrier of (G,yy0), the carrier of (G,yy0):] is set

dom yy0 is countable V167() V168() V169() V170() V171() V172() Element of bool NAT
I . x0 is set

comp (G,j) is Relation-like Function-like non empty V14( the carrier of (G,j)) quasi_total Element of bool [: the carrier of (G,j), the carrier of (G,j):]
the carrier of (G,j) is non empty set
[: the carrier of (G,j), the carrier of (G,j):] is Relation-like set
bool [: the carrier of (G,j), the carrier of (G,j):] is set
seq . x0 is set

Seg (len yy0) is V30() V37( len yy0) countable V167() V168() V169() V170() V171() V172() Element of bool NAT

dom y0 is countable V167() V168() V169() V170() V171() V172() Element of bool NAT

Seg (len y0) is V30() V37( len y0) countable V167() V168() V169() V170() V171() V172() Element of bool NAT

len I is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len (G)) is non empty V30() V37( len (G)) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
dom G is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT
len G is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len G) is non empty V30() V37( len G) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
seq is set

I . yy0 is set

the ZeroF of (G,yy0) is Element of the carrier of (G,yy0)
the carrier of (G,yy0) is non empty set

(G) . y0 is set

the carrier of (G,y0) is non empty set
I . seq is set
(G) . seq is set
dom I is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT
Seg (len I) is non empty V30() V37( len I) countable V167() V168() V169() V170() V171() V172() Element of bool NAT

seq . yy0 is Element of (G) . yy0
(G) . yy0 is non empty set

the ZeroF of (G,yy0) is Element of the carrier of (G,yy0)
the carrier of (G,yy0) is non empty set

x0 is set

yy0 . x0 is set

the ZeroF of (G,j) is Element of the carrier of (G,j)
the carrier of (G,j) is non empty set

y0 . x0 is set
dom yy0 is set
dom y0 is set

len I is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
seq is set
len G is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
dom G is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT

I . yy0 is set

the Mult of (G,yy0) is Relation-like Function-like V14([:REAL, the carrier of (G,yy0):]) quasi_total Element of bool [:[:REAL, the carrier of (G,yy0):], the carrier of (G,yy0):]
the carrier of (G,yy0) is non empty set
[:REAL, the carrier of (G,yy0):] is Relation-like V30() set
[:[:REAL, the carrier of (G,yy0):], the carrier of (G,yy0):] is Relation-like V30() set
bool [:[:REAL, the carrier of (G,yy0):], the carrier of (G,yy0):] is V30() set

the carrier of (G,y0) is non empty set
(G) . y0 is set
I . seq is set
(G) . seq is set
[:REAL,((G) . seq):] is Relation-like set
[:[:REAL,((G) . seq):],((G) . seq):] is Relation-like set
bool [:[:REAL,((G) . seq):],((G) . seq):] is set

(G) . yy0 is non empty set
[:REAL,((G) . yy0):] is Relation-like V30() set

the carrier of (G,yy0) is non empty set
[:REAL, the carrier of (G,yy0):] is Relation-like V30() set
((G),REAL,seq,yy0) is Relation-like Function-like V14([:REAL,((G) . yy0):]) quasi_total Element of bool [:[:REAL,((G) . yy0):],((G) . yy0):]
[:[:REAL,((G) . yy0):],((G) . yy0):] is Relation-like V30() set
bool [:[:REAL,((G) . yy0):],((G) . yy0):] is V30() set
the Mult of (G,yy0) is Relation-like Function-like V14([:REAL, the carrier of (G,yy0):]) quasi_total Element of bool [:[:REAL, the carrier of (G,yy0):], the carrier of (G,yy0):]
[:[:REAL, the carrier of (G,yy0):], the carrier of (G,yy0):] is Relation-like V30() set
bool [:[:REAL, the carrier of (G,yy0):], the carrier of (G,yy0):] is V30() set

dom yy0 is countable V167() V168() V169() V170() V171() V172() Element of bool NAT
yy0 . x0 is set

the Mult of (G,j) is Relation-like Function-like V14([:REAL, the carrier of (G,j):]) quasi_total Element of bool [:[:REAL, the carrier of (G,j):], the carrier of (G,j):]
the carrier of (G,j) is non empty set
[:REAL, the carrier of (G,j):] is Relation-like V30() set
[:[:REAL, the carrier of (G,j):], the carrier of (G,j):] is Relation-like V30() set
bool [:[:REAL, the carrier of (G,j):], the carrier of (G,j):] is V30() set

y0 . x0 is set

Seg (len yy0) is V30() V37( len yy0) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
dom y0 is countable V167() V168() V169() V170() V171() V172() Element of bool NAT

Seg (len y0) is V30() V37( len y0) countable V167() V168() V169() V170() V171() V172() Element of bool NAT

[:(G):] is Relation-like Function-like V14([:(product (G)),(product (G)):]) quasi_total Element of bool [:[:(product (G)),(product (G)):],(product (G)):]
[:(product (G)),(product (G)):] is Relation-like set
[:[:(product (G)),(product (G)):],(product (G)):] is Relation-like set
bool [:[:(product (G)),(product (G)):],(product (G)):] is set

((G),REAL,(G)) is Relation-like Function-like V14([:REAL,(product (G)):]) quasi_total Element of bool [:[:REAL,(product (G)):],(product (G)):]
[:REAL,(product (G)):] is Relation-like V30() set
[:[:REAL,(product (G)):],(product (G)):] is Relation-like V30() set
bool [:[:REAL,(product (G)):],(product (G)):] is V30() set
RLSStruct(# (product (G)),(G),[:(G):],((G),REAL,(G)) #) is non empty strict RLSStruct
the carrier of G is non empty set
the addF of G is Relation-like Function-like V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
I is Element of the carrier of G
seq is Element of the carrier of G
I + seq is Element of the carrier of G
the addF of G . (I,seq) is Element of the carrier of G
seq + I is Element of the carrier of G
the addF of G . (seq,I) is Element of the carrier of G
I is Element of the carrier of G
seq is Element of the carrier of G
I + seq is Element of the carrier of G
the addF of G . (I,seq) is Element of the carrier of G
yy0 is Element of the carrier of G
(I + seq) + yy0 is Element of the carrier of G
the addF of G . ((I + seq),yy0) is Element of the carrier of G
seq + yy0 is Element of the carrier of G
the addF of G . (seq,yy0) is Element of the carrier of G
I + (seq + yy0) is Element of the carrier of G
the addF of G . (I,(seq + yy0)) is Element of the carrier of G
the carrier of G is non empty set
the ZeroF of G is Element of the carrier of G
the addF of G is Relation-like Function-like V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
I is Element of the carrier of G
0. G is V82(G) Element of the carrier of G
I + (0. G) is Element of the carrier of G
the addF of G . (I,(0. G)) is Element of the carrier of G

dom (G) is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT

[:(G):] is Relation-like Function-like V14([:(product (G)),(product (G)):]) quasi_total Element of bool [:[:(product (G)),(product (G)):],(product (G)):]
[:(product (G)),(product (G)):] is Relation-like set
[:[:(product (G)),(product (G)):],(product (G)):] is Relation-like set
bool [:[:(product (G)),(product (G)):],(product (G)):] is set

[:(G):] . (I,seq) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)

([:(G):] . (I,seq)) . yy0 is Element of (G) . yy0
(G) . yy0 is non empty set

the addF of (G,yy0) is Relation-like Function-like V14([: the carrier of (G,yy0), the carrier of (G,yy0):]) quasi_total Element of bool [:[: the carrier of (G,yy0), the carrier of (G,yy0):], the carrier of (G,yy0):]
the carrier of (G,yy0) is non empty set
[: the carrier of (G,yy0), the carrier of (G,yy0):] is Relation-like set
[:[: the carrier of (G,yy0), the carrier of (G,yy0):], the carrier of (G,yy0):] is Relation-like set
bool [:[: the carrier of (G,yy0), the carrier of (G,yy0):], the carrier of (G,yy0):] is set
I . yy0 is Element of (G) . yy0
seq . yy0 is Element of (G) . yy0
the addF of (G,yy0) . ((I . yy0),(seq . yy0)) is set
(G) . yy0 is Relation-like Function-like V14([:((G) . yy0),((G) . yy0):]) quasi_total Element of bool [:[:((G) . yy0),((G) . yy0):],((G) . yy0):]
[:((G) . yy0),((G) . yy0):] is Relation-like set
[:[:((G) . yy0),((G) . yy0):],((G) . yy0):] is Relation-like set
bool [:[:((G) . yy0),((G) . yy0):],((G) . yy0):] is set
((G) . yy0) . ((I . yy0),(seq . yy0)) is Element of (G) . yy0
y0 is Element of the carrier of (G,yy0)
x0 is Element of the carrier of (G,yy0)
y0 + x0 is Element of the carrier of (G,yy0)
the addF of (G,yy0) . (y0,x0) is Element of the carrier of (G,yy0)

dom (G) is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT

((G),REAL,(G)) is Relation-like Function-like V14([:REAL,(product (G)):]) quasi_total Element of bool [:[:REAL,(product (G)):],(product (G)):]
[:REAL,(product (G)):] is Relation-like V30() set
[:[:REAL,(product (G)):],(product (G)):] is Relation-like V30() set
bool [:[:REAL,(product (G)):],(product (G)):] is V30() set
I is V42() real ext-real Element of REAL

((G),REAL,(G)) . (I,seq) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)

(((G),REAL,(G)) . (I,seq)) . yy0 is Element of (G) . yy0
(G) . yy0 is non empty set

the Mult of (G,yy0) is Relation-like Function-like V14([:REAL, the carrier of (G,yy0):]) quasi_total Element of bool [:[:REAL, the carrier of (G,yy0):], the carrier of (G,yy0):]
the carrier of (G,yy0) is non empty set
[:REAL, the carrier of (G,yy0):] is Relation-like V30() set
[:[:REAL, the carrier of (G,yy0):], the carrier of (G,yy0):] is Relation-like V30() set
bool [:[:REAL, the carrier of (G,yy0):], the carrier of (G,yy0):] is V30() set
seq . yy0 is Element of (G) . yy0
the Mult of (G,yy0) . (I,(seq . yy0)) is set
((G),REAL,(G),yy0) is Relation-like Function-like V14([:REAL,((G) . yy0):]) quasi_total Element of bool [:[:REAL,((G) . yy0):],((G) . yy0):]
[:REAL,((G) . yy0):] is Relation-like V30() set
[:[:REAL,((G) . yy0):],((G) . yy0):] is Relation-like V30() set
bool [:[:REAL,((G) . yy0):],((G) . yy0):] is V30() set
((G),REAL,(G),yy0) . (I,(seq . yy0)) is Element of (G) . yy0
y0 is Element of the carrier of (G,yy0)
I * y0 is Element of the carrier of (G,yy0)
the Mult of (G,yy0) . (I,y0) is set

(G) is non empty strict RLSStruct

[:(G):] is Relation-like Function-like V14([:(product (G)),(product (G)):]) quasi_total Element of bool [:[:(product (G)),(product (G)):],(product (G)):]
[:(product (G)),(product (G)):] is Relation-like set
[:[:(product (G)),(product (G)):],(product (G)):] is Relation-like set
bool [:[:(product (G)),(product (G)):],(product (G)):] is set

((G),REAL,(G)) is Relation-like Function-like V14([:REAL,(product (G)):]) quasi_total Element of bool [:[:REAL,(product (G)):],(product (G)):]
[:REAL,(product (G)):] is Relation-like V30() set
[:[:REAL,(product (G)):],(product (G)):] is Relation-like V30() set
bool [:[:REAL,(product (G)):],(product (G)):] is V30() set
RLSStruct(# (product (G)),(G),[:(G):],((G),REAL,(G)) #) is non empty strict RLSStruct
dom G is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT
len G is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len G) is non empty V30() V37( len G) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
len (G) is non empty epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable V167() V168() V169() V170() V171() V172() Element of NAT
Seg (len (G)) is non empty V30() V37( len (G)) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
dom (G) is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT
seq is V42() real ext-real set
yy0 is V42() real ext-real set
I is non empty RLSStruct
the carrier of I is non empty set
j is Element of the carrier of I
i0 is Element of the carrier of I
seqi is set

the carrier of (G,i) is non empty set

seqi . i is Element of (G) . i
(G) . i is non empty set
((G),REAL,(G)) . (1,seqi) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
(((G),REAL,(G)) . (1,seqi)) . seqi is set
seqimx0 is Element of the carrier of (G,i)
1 * seqimx0 is Element of the carrier of (G,i)
the Mult of (G,i) is Relation-like Function-like V14([:REAL, the carrier of (G,i):]) quasi_total Element of bool [:[:REAL, the carrier of (G,i):], the carrier of (G,i):]
[:REAL, the carrier of (G,i):] is Relation-like V30() set
[:[:REAL, the carrier of (G,i):], the carrier of (G,i):] is Relation-like V30() set
bool [:[:REAL, the carrier of (G,i):], the carrier of (G,i):] is V30() set
the Mult of (G,i) . (1,seqimx0) is set
seqi . seqi is set
seqi is set

the carrier of (G,i) is non empty set
seqi . i is Element of (G) . i
(G) . i is non empty set
y0 is V42() real ext-real Element of REAL
x0 is V42() real ext-real Element of REAL
y0 + x0 is V42() real ext-real Element of REAL
((G),REAL,(G)) . ((y0 + x0),seqi) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
(((G),REAL,(G)) . ((y0 + x0),seqi)) . i is Element of (G) . i
seqimx0 is Element of the carrier of (G,i)
(y0 + x0) * seqimx0 is Element of the carrier of (G,i)
the Mult of (G,i) is Relation-like Function-like V14([:REAL, the carrier of (G,i):]) quasi_total Element of bool [:[:REAL, the carrier of (G,i):], the carrier of (G,i):]
[:REAL, the carrier of (G,i):] is Relation-like V30() set
[:[:REAL, the carrier of (G,i):], the carrier of (G,i):] is Relation-like V30() set
bool [:[:REAL, the carrier of (G,i):], the carrier of (G,i):] is V30() set
the Mult of (G,i) . ((y0 + x0),seqimx0) is set
y0 * seqimx0 is Element of the carrier of (G,i)
the Mult of (G,i) . (y0,seqimx0) is set
x0 * seqimx0 is Element of the carrier of (G,i)
the Mult of (G,i) . (x0,seqimx0) is set
(y0 * seqimx0) + (x0 * seqimx0) is Element of the carrier of (G,i)
the addF of (G,i) is Relation-like Function-like V14([: the carrier of (G,i), the carrier of (G,i):]) quasi_total Element of bool [:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):]
[: the carrier of (G,i), the carrier of (G,i):] is Relation-like set
[:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):] is Relation-like set
bool [:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):] is set
the addF of (G,i) . ((y0 * seqimx0),(x0 * seqimx0)) is Element of the carrier of (G,i)
((G),REAL,(G)) . (y0,seqi) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
(((G),REAL,(G)) . (y0,seqi)) . i is Element of (G) . i
H1((G,i)) . (((((G),REAL,(G)) . (y0,seqi)) . i),(x0 * seqimx0)) is set
((G),REAL,(G)) . (x0,seqi) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
(((G),REAL,(G)) . (x0,seqi)) . i is Element of (G) . i
H1((G,i)) . (((((G),REAL,(G)) . (y0,seqi)) . i),((((G),REAL,(G)) . (x0,seqi)) . i)) is set
(((G),REAL,(G)) . ((y0 + x0),seqi)) . seqi is set
[:(G):] . ((((G),REAL,(G)) . (y0,seqi)),(((G),REAL,(G)) . (x0,seqi))) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
([:(G):] . ((((G),REAL,(G)) . (y0,seqi)),(((G),REAL,(G)) . (x0,seqi)))) . seqi is set
seqi is set

the carrier of (G,i) is non empty set
seqi . i is Element of (G) . i
(G) . i is non empty set

seqi . i is Element of (G) . i
[:(G):] . (seqi,seqi) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
((G),REAL,(G)) . (y0,([:(G):] . (seqi,seqi))) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
(((G),REAL,(G)) . (y0,([:(G):] . (seqi,seqi)))) . i is Element of (G) . i
the Mult of (G,i) is Relation-like Function-like V14([:REAL, the carrier of (G,i):]) quasi_total Element of bool [:[:REAL, the carrier of (G,i):], the carrier of (G,i):]
[:REAL, the carrier of (G,i):] is Relation-like V30() set
[:[:REAL, the carrier of (G,i):], the carrier of (G,i):] is Relation-like V30() set
bool [:[:REAL, the carrier of (G,i):], the carrier of (G,i):] is V30()