:: PRVECT_2 semantic presentation

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

NAT is non empty epsilon-transitive epsilon-connected ordinal V30() V35() V36() countable denumerable V167() V168() V169() V170() V171() V172() V173() Element of bool REAL

bool REAL is V30() set

{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V42() real ext-real complex-yielding V48() V49() V50() Cardinal-yielding countable V167() V168() V169() V170() V171() V172() V173() 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

[:COMPLEX,COMPLEX:] is Relation-like V30() complex-yielding set

bool [:COMPLEX,COMPLEX:] is V30() set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like V30() complex-yielding set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is V30() set

[:REAL,REAL:] is Relation-like V30() complex-yielding V48() V49() set

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

[:[:REAL,REAL:],REAL:] is Relation-like V30() complex-yielding V48() V49() set

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

[:RAT,RAT:] is Relation-like RAT -valued V30() complex-yielding V48() V49() set

bool [:RAT,RAT:] is V30() set

[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued V30() complex-yielding V48() V49() set

bool [:[:RAT,RAT:],RAT:] is V30() set

[:INT,INT:] is Relation-like RAT -valued INT -valued V30() complex-yielding V48() V49() set

bool [:INT,INT:] is V30() set

[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued V30() complex-yielding V48() V49() set

bool [:[:INT,INT:],INT:] is V30() set

[:NAT,NAT:] is Relation-like RAT -valued INT -valued V30() complex-yielding V48() V49() V50() set

[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued V30() complex-yielding V48() V49() V50() set

bool [:[:NAT,NAT:],NAT:] is V30() set

[:NAT,REAL:] is Relation-like V30() complex-yielding V48() V49() set

bool [:NAT,REAL:] 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():] is Relation-like V30() 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

[:[:K421(),K421():],REAL:] is Relation-like complex-yielding V48() V49() set

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

the_set_of_l1RealSequences is Element of bool the carrier of K417()

[:the_set_of_l1RealSequences,REAL:] is Relation-like complex-yielding V48() V49() set

bool [:the_set_of_l1RealSequences,REAL:] is set

[:1,1:] is Relation-like RAT -valued INT -valued complex-yielding V48() V49() V50() set

bool [:1,1:] is set

[:[:1,1:],1:] is Relation-like RAT -valued INT -valued complex-yielding V48() V49() V50() set

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

[:[:1,1:],REAL:] is Relation-like complex-yielding V48() V49() 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

[:2,2:] is Relation-like RAT -valued INT -valued complex-yielding V48() V49() V50() set

[:[:2,2:],REAL:] is Relation-like complex-yielding V48() V49() set

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

TOP-REAL 2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() TopSpace-like V206() L20()

the carrier of (TOP-REAL 2) is non empty set

0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V42() real ext-real complex-yielding V48() V49() V50() V59() V60() Cardinal-yielding countable V167() V168() V169() V170() V171() V172() V173() Element of NAT

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

sqrt 0 is V42() real ext-real Element of REAL

I is Relation-like Function-like non empty V14( NAT ) quasi_total complex-yielding V48() V49() Element of bool [:NAT,REAL:]

G is Relation-like Function-like non empty V14( NAT ) quasi_total complex-yielding V48() V49() Element of bool [:NAT,REAL:]

lim G is V42() real ext-real Element of REAL

lim I is V42() real ext-real Element of REAL

seq is V42() real ext-real set

yy0 is V42() real ext-real set

y0 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

x0 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

j 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

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

j 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

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

y0 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

x0 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

j 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

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

j 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

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

G is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable FinSequence of REAL

len G 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

I is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable FinSequence of REAL

len I 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

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

sqr G is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable FinSequence 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

sqr I is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable FinSequence 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

seq is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real countable set

(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

len (sqr I) 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

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

len (sqr G) 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

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

(len (sqr G)) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL

REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL

{ b

(len (sqr I)) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL

{ b

G is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable FinSequence of REAL

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

Sum G is V42() real ext-real Element of REAL

len G 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

(len G) |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() V50() countable Element of (len G) -tuples_on NAT

(len G) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT

NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT

{ b

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

K106((Seg (len G)),0) is Relation-like NAT -defined RAT -valued INT -valued Function-like V14( Seg (len G)) quasi_total V30() FinSequence-like FinSubsequence-like complex-yielding V48() V49() V50() Cardinal-yielding countable Element of bool [:(Seg (len G)),{0}:]

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

[:(Seg (len G)),{0}:] is Relation-like RAT -valued INT -valued complex-yielding V48() V49() V50() set

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

(len G) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL

REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL

{ b

yy0 is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of (len G) -tuples_on REAL

y0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real countable set

((len G) |-> 0) . y0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V42() real ext-real complex-yielding V48() V49() V50() Cardinal-yielding countable V167() V168() V169() V170() V171() V172() V173() Element of REAL

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

G is Relation-like Function-like set

dom G is set

I is set

seq is Relation-like Function-like 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):]

G is Relation-like non-empty NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable set

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

I is Relation-like non-empty NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable 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

seq is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable set

len seq 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 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

G is Relation-like non-empty NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable set

I is set

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

seq is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable (G,I)

yy0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

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

I is Relation-like non-empty NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable set

product I is functional non empty with_common_domain product-like set

[:G,(product I):] is Relation-like set

[:[:G,(product I):],(product I):] is Relation-like set

bool [:[:G,(product I):],(product I):] 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,(product I):]) quasi_total Element of bool [:[:G,(product I):],(product I):]

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

y0 is Element of G

x0 is Relation-like NAT -defined Function-like I -compatible Element of product I

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

G is Relation-like non-empty NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable set

I is non empty set

product G is functional non empty with_common_domain product-like set

[:I,(product G):] is Relation-like set

[:[:I,(product G):],(product G):] is Relation-like set

bool [:[:I,(product G):],(product G):] is set

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

seq is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable (G,I)

yy0 is Element of I

y0 is Relation-like NAT -defined Function-like G -compatible Element of product G

x0 is set

j is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

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

x0 is Relation-like Function-like set

dom x0 is set

j is set

x0 . j is set

G . j is set

i0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

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 is Relation-like NAT -defined Function-like G -compatible Element of product G

i0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

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

seqi is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

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,(product G):]) quasi_total Element of bool [:[:I,(product G):],(product G):]

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

x0 is Element of I

j is Relation-like NAT -defined Function-like G -compatible Element of product G

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

i0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom 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) is Relation-like NAT -defined Function-like G -compatible Element of product G

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

the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

<* the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct *> is Relation-like NAT -defined Function-like constant non empty trivial V30() V37(1) FinSequence-like FinSubsequence-like countable set

I is set

rng <* the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct *> is non empty trivial V37(1) set

{ the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct } is non empty trivial V37(1) set

G is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () set

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

I is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

G . I is set

rng G is non empty set

G is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () 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

I is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real countable set

seq is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

(G,seq) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

I is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable 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

yy0 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

I . yy0 is set

y0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

(G,y0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

seq is Relation-like non-empty NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable 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

yy0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

seq . yy0 is set

(G,yy0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

y0 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

seq . y0 is set

x0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

(G,x0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

I is Relation-like non-empty NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable 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 Relation-like non-empty NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable 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

x0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real countable set

yy0 is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable set

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

yy0 . x0 is set

j is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

(G,j) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

y0 is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable set

y0 . x0 is set

len yy0 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

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

len y0 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

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

G is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () set

(G) is Relation-like non-empty NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable set

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

I is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

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

seq is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

(G,seq) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

G is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () set

(G) is Relation-like non-empty NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable 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 is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable 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 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

seq is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

I . seq is set

(G,seq) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

yy0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

(G,yy0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

seq is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable BinOps of (G)

len seq 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

yy0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

(G) . yy0 is non empty set

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

(G,yy0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

I is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable BinOps of (G)

len I 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

seq is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable BinOps of (G)

len seq 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

x0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real countable set

yy0 is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable set

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

yy0 . x0 is set

j is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

(G,j) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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 is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable set

y0 . x0 is set

len yy0 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

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

len y0 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

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

I is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable 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 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

seq is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

I . seq is set

(G,seq) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

yy0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

(G,yy0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

seq is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable UnOps of (G)

len seq 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

yy0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

(G) . yy0 is non empty set

(G,yy0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

I is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable UnOps of (G)

len I 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

seq is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable UnOps of (G)

len seq 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

x0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real countable set

yy0 is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable set

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

I . x0 is set

j is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

(G,j) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

len yy0 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

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

y0 is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable set

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

len y0 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

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

product (G) is functional non empty with_common_domain product-like set

I is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable 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

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

yy0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

I . yy0 is set

(G,yy0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

the ZeroF of (G,yy0) is Element of the carrier of (G,yy0)

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

y0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

(G) . y0 is set

(G,y0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)

yy0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

seq . yy0 is Element of (G) . yy0

(G) . yy0 is non empty set

(G,yy0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

the ZeroF of (G,yy0) is Element of the carrier of (G,yy0)

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

I is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)

seq is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)

x0 is set

yy0 is Relation-like Function-like set

yy0 . x0 is set

j is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

(G,j) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

the ZeroF of (G,j) is Element of the carrier of (G,j)

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

y0 is Relation-like Function-like set

y0 . x0 is set

dom yy0 is set

dom y0 is set

I is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable 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

yy0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

I . yy0 is set

(G,yy0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

y0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G

(G,y0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

seq is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable ((G), REAL )

len seq 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

yy0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

(G) . yy0 is non empty set

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

(G,yy0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

I is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable ((G), REAL )

len I 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

seq is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable ((G), REAL )

len seq 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

x0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real countable set

yy0 is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable set

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

yy0 . x0 is set

j is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

(G,j) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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 is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable set

y0 . x0 is set

len yy0 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

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

len y0 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

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

G is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () set

(G) is Relation-like non-empty NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable set

product (G) is functional non empty with_common_domain product-like set

(G) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)

(G) is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable BinOps of (G)

[:(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) is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable ((G), REAL )

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

G is non empty addLoopStr

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

G is non empty addLoopStr

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

G is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () set

(G) is Relation-like non-empty NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable set

product (G) is functional non empty with_common_domain product-like set

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

(G) is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable BinOps of (G)

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

I is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)

seq is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)

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

yy0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

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

(G) . yy0 is non empty set

(G,yy0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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)

G is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () set

(G) is Relation-like non-empty NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable set

product (G) is functional non empty with_common_domain product-like set

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

(G) is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable ((G), REAL )

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

seq is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)

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

yy0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

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

(G) . yy0 is non empty set

(G,yy0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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 Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () set

(G) is non empty strict RLSStruct

(G) is Relation-like non-empty NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable set

product (G) is functional non empty with_common_domain product-like set

(G) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)

(G) is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable BinOps of (G)

[:(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) is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable ((G), REAL )

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

i is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

(G,i) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

seqi is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)

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

i is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

(G,i) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

H

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

H

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

i is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)

(G,i) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct

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

seqi . i is Element of (G) . i

(G) . i is non empty set

seqi is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)

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