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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len (sqr G) } is set
(len (sqr I)) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len (sqr I) } is set
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
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of NAT * : len b1 = len G } is set
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len G } is set
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
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
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() set
([:(G):] . (seqi,seqi)) . i is Element of (G) . i
the Mult of (G,i) . (y0,(([:(G):] . (seqi,seqi)) . i)) is set
seqimx0 is Element of the carrier of (G,i)
mx0 is Element of the carrier of (G,i)
seqimx0 + mx0 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) . (seqimx0,mx0) is Element of the carrier of (G,i)
y0 * (seqimx0 + mx0) is Element of the carrier of (G,i)
the Mult of (G,i) . (y0,(seqimx0 + mx0)) is set
y0 * seqimx0 is Element of the carrier of (G,i)
the Mult of (G,i) . (y0,seqimx0) is set
y0 * mx0 is Element of the carrier of (G,i)
the Mult of (G,i) . (y0,mx0) is set
(y0 * seqimx0) + (y0 * mx0) is Element of the carrier of (G,i)
the addF of (G,i) . ((y0 * seqimx0),(y0 * mx0)) is Element of the carrier of (G,i)
(((G),REAL,(G)) . (y0,seqi)) . i is Element of (G) . i
H1((G,i)) . (((((G),REAL,(G)) . (y0,seqi)) . i),(y0 * mx0)) is set
((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),((((G),REAL,(G)) . (y0,seqi)) . i)) is set
(((G),REAL,(G)) . (y0,([:(G):] . (seqi,seqi)))) . seqi is set
[:(G):] . ((((G),REAL,(G)) . (y0,seqi)),(((G),REAL,(G)) . (y0,seqi))) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
([:(G):] . ((((G),REAL,(G)) . (y0,seqi)),(((G),REAL,(G)) . (y0,seqi)))) . seqi is set
dom (((G),REAL,(G)) . (y0,([:(G):] . (seqi,seqi)))) is set
dom ([:(G):] . ((((G),REAL,(G)) . (y0,seqi)),(((G),REAL,(G)) . (y0,seqi)))) is set
j + i0 is Element of the carrier of I
the addF of I is Relation-like Function-like V14([: the carrier of I, the carrier of I:]) quasi_total Element of bool [:[: the carrier of I, the carrier of I:], the carrier of I:]
[: the carrier of I, the carrier of I:] is Relation-like set
[:[: the carrier of I, the carrier of I:], the carrier of I:] is Relation-like set
bool [:[: the carrier of I, the carrier of I:], the carrier of I:] is set
the addF of I . (j,i0) is Element of the carrier of I
seq * (j + i0) is Element of the carrier of I
the Mult of I is Relation-like Function-like V14([:REAL, the carrier of I:]) quasi_total Element of bool [:[:REAL, the carrier of I:], the carrier of I:]
[:REAL, the carrier of I:] is Relation-like V30() set
[:[:REAL, the carrier of I:], the carrier of I:] is Relation-like V30() set
bool [:[:REAL, the carrier of I:], the carrier of I:] is V30() set
the Mult of I . (seq,(j + i0)) is set
seq * j is Element of the carrier of I
the Mult of I . (seq,j) is set
seq * i0 is Element of the carrier of I
the Mult of I . (seq,i0) is set
(seq * j) + (seq * i0) is Element of the carrier of I
the addF of I . ((seq * j),(seq * 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 . i is Element of (G) . i
(G) . i is non empty set
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
x0 * seqimx0 is Element of the carrier of (G,i)
the Mult of (G,i) . (x0,seqimx0) is set
y0 * (x0 * seqimx0) is Element of the carrier of (G,i)
the Mult of (G,i) . (y0,(x0 * seqimx0)) is set
(((G),REAL,(G)) . (x0,seqi)) . i is Element of (G) . i
the Mult of (G,i) . (y0,((((G),REAL,(G)) . (x0,seqi)) . i)) is set
(((G),REAL,(G)) . ((y0 * x0),seqi)) . seqi is set
((G),REAL,(G)) . (y0,(((G),REAL,(G)) . (x0,seqi))) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
(((G),REAL,(G)) . (y0,(((G),REAL,(G)) . (x0,seqi)))) . seqi is set
dom (((G),REAL,(G)) . ((y0 + x0),seqi)) is set
dom ([:(G):] . ((((G),REAL,(G)) . (y0,seqi)),(((G),REAL,(G)) . (x0,seqi)))) is set
seq + yy0 is V42() real ext-real set
(seq + yy0) * j is Element of the carrier of I
the Mult of I . ((seq + yy0),j) is set
yy0 * j is Element of the carrier of I
the Mult of I . (yy0,j) is set
(seq * j) + (yy0 * j) is Element of the carrier of I
the addF of I . ((seq * j),(yy0 * j)) is Element of the carrier of I
dom (((G),REAL,(G)) . ((y0 * x0),seqi)) is set
dom (((G),REAL,(G)) . (y0,(((G),REAL,(G)) . (x0,seqi)))) is set
seq * yy0 is V42() real ext-real set
(seq * yy0) * j is Element of the carrier of I
the Mult of I . ((seq * yy0),j) is set
seq * (yy0 * j) is Element of the carrier of I
the Mult of I . (seq,(yy0 * j)) is set
dom (((G),REAL,(G)) . (1,seqi)) is set
dom seqi is set
1 * j is Element of the carrier of I
the Mult of I . (1,j) 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
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 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 carrier of (G,seq) is non empty 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 set
[:((G) . seq),((G) . seq):] is Relation-like 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 carrier of (G,seq) is non empty set
[: the carrier of (G,seq), the carrier of (G,seq):] is Relation-like set
(G) . seq is Relation-like Function-like V14([:((G) . seq),((G) . seq):]) quasi_total Element of bool [:[:((G) . seq),((G) . seq):],((G) . seq):]
[:[:((G) . seq),((G) . seq):],((G) . seq):] is Relation-like set
bool [:[:((G) . seq),((G) . seq):],((G) . 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), 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
seq is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)
(G) . seq is Element of (G) . seq
(G) . seq is non empty 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
0. (G,seq) is V82((G,seq)) Element of the carrier of (G,seq)
the carrier of (G,seq) is non empty set
the ZeroF of (G,seq) is Element of the carrier of (G,seq)
[:((G) . seq),((G) . seq):] is Relation-like set
[: the carrier of (G,seq), the carrier of (G,seq):] is Relation-like set
(G) . seq is Relation-like Function-like V14([:((G) . seq),((G) . seq):]) quasi_total Element of bool [:[:((G) . seq),((G) . seq):],((G) . seq):]
[:[:((G) . seq),((G) . seq):],((G) . seq):] is Relation-like set
bool [:[:((G) . seq),((G) . seq):],((G) . 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), 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
I is non empty RLSStruct
the carrier of I is non empty set
seq is Element of the carrier of I
(G) is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable UnOps of (G)
Frege (G) is Relation-like Function-like non empty V14( product (G)) quasi_total Element of bool [:(product (G)),(product (G)):]
bool [:(product (G)),(product (G)):] is set
(Frege (G)) . seq is set
yy0 is Element of the carrier of I
seq + yy0 is Element of the carrier of I
the addF of I is Relation-like Function-like V14([: the carrier of I, the carrier of I:]) quasi_total Element of bool [:[: the carrier of I, the carrier of I:], the carrier of I:]
[: the carrier of I, the carrier of I:] is Relation-like set
[:[: the carrier of I, the carrier of I:], the carrier of I:] is Relation-like set
bool [:[: the carrier of I, the carrier of I:], the carrier of I:] is set
the addF of I . (seq,yy0) is Element of the carrier of I
0. I is V82(I) Element of the carrier of I
the ZeroF of I is Element of the carrier of I
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
0. (G,y0) is V82((G,y0)) Element of the carrier of (G,y0)
the carrier of (G,y0) is non empty set
the ZeroF of (G,y0) is Element of the carrier of (G,y0)
the addF of (G,y0) is Relation-like Function-like V14([: the carrier of (G,y0), the carrier of (G,y0):]) quasi_total Element of bool [:[: the carrier of (G,y0), the carrier of (G,y0):], the carrier of (G,y0):]
[: the carrier of (G,y0), the carrier of (G,y0):] is Relation-like set
[:[: the carrier of (G,y0), the carrier of (G,y0):], the carrier of (G,y0):] is Relation-like set
bool [:[: the carrier of (G,y0), the carrier of (G,y0):], the carrier of (G,y0):] is set
(G) . y0 is non empty set
(G) . y0 is Relation-like Function-like non empty V14((G) . y0) quasi_total Element of bool [:((G) . y0),((G) . y0):]
[:((G) . y0),((G) . y0):] is Relation-like set
bool [:((G) . y0),((G) . y0):] is set
comp (G,y0) is Relation-like Function-like non empty V14( the carrier of (G,y0)) quasi_total Element of bool [: the carrier of (G,y0), the carrier of (G,y0):]
bool [: the carrier of (G,y0), the carrier of (G,y0):] is set
(G) . y0 is Relation-like Function-like V14([:((G) . y0),((G) . y0):]) quasi_total Element of bool [:[:((G) . y0),((G) . y0):],((G) . y0):]
[:[:((G) . y0),((G) . y0):],((G) . y0):] is Relation-like set
bool [:[:((G) . y0),((G) . y0):],((G) . y0):] is set
[:(G):] . (seq,yy0) is set
the_unity_wrt [:(G):] is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
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 set
[:((G) . seq),((G) . seq):] is Relation-like 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 carrier of (G,seq) is non empty set
[: the carrier of (G,seq), the carrier of (G,seq):] is Relation-like set
(G) . seq is Relation-like Function-like V14([:((G) . seq),((G) . seq):]) quasi_total Element of bool [:[:((G) . seq),((G) . seq):],((G) . seq):]
[:[:((G) . seq),((G) . seq):],((G) . seq):] is Relation-like set
bool [:[:((G) . seq),((G) . seq):],((G) . 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), 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 non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR
<* the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR *> 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() discerning reflexive RealNormSpace-like NORMSTR *> 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() discerning reflexive RealNormSpace-like NORMSTR } 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 V30() FinSequence-like FinSubsequence-like countable () set
rng G is set
I is set
G is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable set
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
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
REAL (len G) is functional non empty FinSequence-membered FinSequenceSet of REAL
(len G) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len G } is set
dom G is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT
I is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
[:(dom G),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [:(dom G),REAL:] is V30() set
seq is Relation-like Function-like non empty V14( dom G) quasi_total complex-yielding V48() V49() Element of bool [:(dom G),REAL:]
rng seq is non empty V167() V168() V169() Element of bool REAL
dom seq is non empty set
Seg (len G) is non empty V30() V37( len G) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
yy0 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable FinSequence of REAL
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
y0 is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
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
x0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G
y0 . x0 is V42() real ext-real Element of REAL
(G,x0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR
the normF of (G,x0) is Relation-like Function-like non empty V14( the carrier of (G,x0)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G,x0),REAL:]
the carrier of (G,x0) is non empty set
[: the carrier of (G,x0),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G,x0),REAL:] is V30() set
I . x0 is set
the normF of (G,x0) . (I . x0) is V42() real ext-real Element of REAL
seq is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len 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 Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
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
y0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real countable set
Seg (len G) is non empty V30() V37( len G) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
seq . y0 is V42() real ext-real Element of REAL
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() discerning reflexive RealNormSpace-like NORMSTR
the normF of (G,x0) is Relation-like Function-like non empty V14( the carrier of (G,x0)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G,x0),REAL:]
the carrier of (G,x0) is non empty set
[: the carrier of (G,x0),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G,x0),REAL:] is V30() set
I . x0 is set
the normF of (G,x0) . (I . x0) is V42() real ext-real Element of REAL
yy0 . y0 is V42() real ext-real Element of REAL
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
[:(product (G)),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [:(product (G)),REAL:] is V30() set
I is Relation-like Function-like non empty V14( product (G)) quasi_total complex-yielding V48() V49() Element of bool [:(product (G)),REAL:]
seq is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
I . seq is V42() real ext-real Element of REAL
(G,seq) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
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
REAL (len G) is functional non empty FinSequence-membered FinSequenceSet of REAL
(len G) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len G } is set
|.(G,seq).| is V42() real ext-real non negative Element of REAL
sqr (G,seq) 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,seq)) is V42() real ext-real Element of REAL
sqrt (Sum (sqr (G,seq))) is V42() real ext-real Element of REAL
I is Relation-like Function-like non empty V14( product (G)) quasi_total complex-yielding V48() V49() Element of bool [:(product (G)),REAL:]
seq is Relation-like Function-like non empty V14( product (G)) quasi_total complex-yielding V48() V49() Element of bool [:(product (G)),REAL:]
yy0 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
I . yy0 is V42() real ext-real Element of REAL
(G,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 REAL (len G)
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
REAL (len G) is functional non empty FinSequence-membered FinSequenceSet of REAL
(len G) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len G } is set
|.(G,yy0).| is V42() real ext-real non negative Element of REAL
sqr (G,yy0) 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,yy0)) is V42() real ext-real Element of REAL
sqrt (Sum (sqr (G,yy0))) is V42() real ext-real Element of REAL
seq . yy0 is V42() real ext-real Element of REAL
G is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () () set
(G) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() 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
(G) is Relation-like Function-like non empty V14( product (G)) quasi_total complex-yielding V48() V49() Element of bool [:(product (G)),REAL:]
[:(product (G)),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [:(product (G)),REAL:] is V30() set
NORMSTR(# (product (G)),(G),[:(G):],((G),REAL,(G)),(G) #) is strict NORMSTR
I is non empty strict NORMSTR
the carrier of I is non empty set
the ZeroF of I is Element of the carrier of I
the addF of I is Relation-like Function-like V14([: the carrier of I, the carrier of I:]) quasi_total Element of bool [:[: the carrier of I, the carrier of I:], the carrier of I:]
[: the carrier of I, the carrier of I:] is Relation-like set
[:[: the carrier of I, the carrier of I:], the carrier of I:] is Relation-like set
bool [:[: the carrier of I, the carrier of I:], the carrier of I:] is set
the Mult of I is Relation-like Function-like V14([:REAL, the carrier of I:]) quasi_total Element of bool [:[:REAL, the carrier of I:], the carrier of I:]
[:REAL, the carrier of I:] is Relation-like V30() set
[:[:REAL, the carrier of I:], the carrier of I:] is Relation-like V30() set
bool [:[:REAL, the carrier of I:], the carrier of I:] is V30() set
RLSStruct(# the carrier of I, the ZeroF of I, the addF of I, the Mult of I #) is non empty strict RLSStruct
the normF of I is Relation-like Function-like non empty V14( the carrier of I) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of I,REAL:]
[: the carrier of I,REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of I,REAL:] is V30() set
I is non empty strict NORMSTR
the carrier of I is non empty set
the ZeroF of I is Element of the carrier of I
the addF of I is Relation-like Function-like V14([: the carrier of I, the carrier of I:]) quasi_total Element of bool [:[: the carrier of I, the carrier of I:], the carrier of I:]
[: the carrier of I, the carrier of I:] is Relation-like set
[:[: the carrier of I, the carrier of I:], the carrier of I:] is Relation-like set
bool [:[: the carrier of I, the carrier of I:], the carrier of I:] is set
the Mult of I is Relation-like Function-like V14([:REAL, the carrier of I:]) quasi_total Element of bool [:[:REAL, the carrier of I:], the carrier of I:]
[:REAL, the carrier of I:] is Relation-like V30() set
[:[:REAL, the carrier of I:], the carrier of I:] is Relation-like V30() set
bool [:[:REAL, the carrier of I:], the carrier of I:] is V30() set
RLSStruct(# the carrier of I, the ZeroF of I, the addF of I, the Mult of I #) is non empty strict RLSStruct
the normF of I is Relation-like Function-like non empty V14( the carrier of I) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of I,REAL:]
[: the carrier of I,REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of I,REAL:] is V30() set
seq is non empty strict NORMSTR
the carrier of seq is non empty set
the ZeroF of seq is Element of the carrier of seq
the addF of seq is Relation-like Function-like V14([: the carrier of seq, the carrier of seq:]) quasi_total Element of bool [:[: the carrier of seq, the carrier of seq:], the carrier of seq:]
[: the carrier of seq, the carrier of seq:] is Relation-like set
[:[: the carrier of seq, the carrier of seq:], the carrier of seq:] is Relation-like set
bool [:[: the carrier of seq, the carrier of seq:], the carrier of seq:] is set
the Mult of seq is Relation-like Function-like V14([:REAL, the carrier of seq:]) quasi_total Element of bool [:[:REAL, the carrier of seq:], the carrier of seq:]
[:REAL, the carrier of seq:] is Relation-like V30() set
[:[:REAL, the carrier of seq:], the carrier of seq:] is Relation-like V30() set
bool [:[:REAL, the carrier of seq:], the carrier of seq:] is V30() set
RLSStruct(# the carrier of seq, the ZeroF of seq, the addF of seq, the Mult of seq #) is non empty strict RLSStruct
the normF of seq is Relation-like Function-like non empty V14( the carrier of seq) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of seq,REAL:]
[: the carrier of seq,REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of seq,REAL:] is V30() set
G is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () () set
(G) is non empty strict NORMSTR
(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
(G) is Relation-like Function-like non empty V14( product (G)) quasi_total complex-yielding V48() V49() Element of bool [:(product (G)),REAL:]
[:(product (G)),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [:(product (G)),REAL:] is V30() set
NORMSTR(# (product (G)),(G),[:(G):],((G),REAL,(G)),(G) #) is strict NORMSTR
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
the Mult of (G) is Relation-like Function-like V14([:REAL, the carrier of (G):]) quasi_total Element of bool [:[:REAL, the carrier of (G):], the carrier of (G):]
[:REAL, the carrier of (G):] is Relation-like V30() set
[:[:REAL, the carrier of (G):], the carrier of (G):] is Relation-like V30() set
bool [:[:REAL, the carrier of (G):], the carrier of (G):] is V30() set
RLSStruct(# the carrier of (G), the ZeroF of (G), the addF of (G), the Mult of (G) #) is non empty strict RLSStruct
(G) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct
RLSStruct(# (product (G)),(G),[:(G):],((G),REAL,(G)) #) is non empty strict RLSStruct
G is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () () set
(G) is non empty strict NORMSTR
the carrier of (G) is non empty 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
I is Element of the carrier of (G)
||.I.|| is V42() real ext-real Element of REAL
the normF of (G) is Relation-like Function-like non empty V14( the carrier of (G)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G),REAL:]
[: the carrier of (G),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G),REAL:] is V30() set
the normF of (G) . I is V42() real ext-real Element of REAL
seq is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
(G,seq) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
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
REAL (len G) is functional non empty FinSequence-membered FinSequenceSet of REAL
(len G) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len G } is set
|.(G,seq).| is V42() real ext-real non negative Element of REAL
sqr (G,seq) 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,seq)) is V42() real ext-real Element of REAL
sqrt (Sum (sqr (G,seq))) is V42() real ext-real Element of REAL
(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
(G) is Relation-like Function-like non empty V14( product (G)) quasi_total complex-yielding V48() V49() Element of bool [:(product (G)),REAL:]
[:(product (G)),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [:(product (G)),REAL:] is V30() set
NORMSTR(# (product (G)),(G),[:(G):],((G),REAL,(G)),(G) #) is strict NORMSTR
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 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
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
I is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
dom I is set
yy0 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)
(G,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 REAL (len G)
REAL (len G) is functional non empty FinSequence-membered FinSequenceSet of REAL
(len G) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len G } is set
(G,I) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
(G,seq) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
(G,I) + (G,seq) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
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
(G,yy0) . y0 is V42() real ext-real Element of REAL
((G,I) + (G,seq)) . y0 is V42() real ext-real Element of REAL
dom (G) is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT
x0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)
yy0 . x0 is Element of (G) . x0
(G) . x0 is non empty set
(G) . x0 is Relation-like Function-like V14([:((G) . x0),((G) . x0):]) quasi_total Element of bool [:[:((G) . x0),((G) . x0):],((G) . x0):]
[:((G) . x0),((G) . x0):] is Relation-like set
[:[:((G) . x0),((G) . x0):],((G) . x0):] is Relation-like set
bool [:[:((G) . x0),((G) . x0):],((G) . x0):] is set
I . x0 is Element of (G) . x0
seq . x0 is Element of (G) . x0
((G) . x0) . ((I . x0),(seq . x0)) is Element of (G) . x0
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
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
j is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G
(G) . j is set
(G,j) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,j) is non empty set
I . j is set
seq . j is set
yy0 . j is set
seqi is Element of the carrier of (G,j)
||.seqi.|| is V42() real ext-real non negative Element of REAL
the normF of (G,j) is Relation-like Function-like non empty V14( the carrier of (G,j)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G,j),REAL:]
[: the carrier of (G,j),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G,j),REAL:] is V30() set
the normF of (G,j) . seqi is V42() real ext-real Element of REAL
i0 is Element of the carrier of (G,j)
seqi is Element of the carrier of (G,j)
i0 + seqi is Element of the carrier of (G,j)
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), 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
the addF of (G,j) . (i0,seqi) is Element of the carrier of (G,j)
||.(i0 + seqi).|| is V42() real ext-real non negative Element of REAL
the normF of (G,j) . (i0 + seqi) is V42() real ext-real Element of REAL
||.i0.|| is V42() real ext-real non negative Element of REAL
the normF of (G,j) . i0 is V42() real ext-real Element of REAL
||.seqi.|| is V42() real ext-real non negative Element of REAL
the normF of (G,j) . seqi is V42() real ext-real Element of REAL
||.i0.|| + ||.seqi.|| is V42() real ext-real non negative Element of REAL
(G,I) . j is V42() real ext-real Element of REAL
(G,seq) . j is V42() real ext-real Element of REAL
((G,I) . j) + ((G,seq) . j) is V42() real ext-real Element of REAL
((G,I) + (G,seq)) . j is V42() real ext-real Element of REAL
the normF of (G,j) . seqi is V42() real ext-real Element of REAL
the normF of (G,j) . seqi is V42() real ext-real Element of REAL
(G,yy0) . j is V42() real ext-real Element of REAL
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
I is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
dom I is set
(G,I) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
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
REAL (len G) is functional non empty FinSequence-membered FinSequenceSet of REAL
(len G) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len G } is set
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
(G,I) . seq is V42() real ext-real Element of REAL
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
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
yy0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G
(G) . 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() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,yy0) is non empty set
I . yy0 is set
y0 is Element of the carrier of (G,yy0)
||.y0.|| is V42() real ext-real non negative Element of REAL
the normF of (G,yy0) is Relation-like Function-like non empty V14( the carrier of (G,yy0)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G,yy0),REAL:]
[: the carrier of (G,yy0),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G,yy0),REAL:] is V30() set
the normF of (G,yy0) . y0 is V42() real ext-real Element of REAL
G is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () () set
(G) is non empty strict NORMSTR
(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
(G) is Relation-like Function-like non empty V14( product (G)) quasi_total complex-yielding V48() V49() Element of bool [:(product (G)),REAL:]
[:(product (G)),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [:(product (G)),REAL:] is V30() set
NORMSTR(# (product (G)),(G),[:(G):],((G),REAL,(G)),(G) #) is strict NORMSTR
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
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
0. (G) is V82((G)) 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)
dom (G) is non empty 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)
(G,seq) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
REAL (len G) is functional non empty FinSequence-membered FinSequenceSet of REAL
(len G) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len G } is set
yy0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)
(G,seq) . yy0 is V42() real ext-real Element of REAL
dom G is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT
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() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,y0) is non empty set
seq . y0 is set
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
0. (G,yy0) is V82((G,yy0)) Element of the carrier of (G,yy0)
the carrier of (G,yy0) is non empty set
the ZeroF of (G,yy0) is Element of the carrier of (G,yy0)
x0 is Element of the carrier of (G,y0)
||.x0.|| is V42() real ext-real non negative Element of REAL
the normF of (G,y0) is Relation-like Function-like non empty V14( the carrier of (G,y0)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G,y0),REAL:]
[: the carrier of (G,y0),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G,y0),REAL:] is V30() set
the normF of (G,y0) . x0 is V42() real ext-real Element of REAL
sqr (G,seq) 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
dom (sqr (G,seq)) is V37( len G) 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 V167() V168() V169() V170() V171() V172() Element of NAT
(sqr (G,seq)) . yy0 is V42() real ext-real Element of REAL
len (G,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 (G,seq) is 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
(G,seq) . yy0 is V42() real ext-real Element of REAL
((G,seq) . yy0) ^2 is V42() real ext-real Element of REAL
((G,seq) . yy0) * ((G,seq) . yy0) is V42() real ext-real set
0 ^2 is V42() real ext-real Element of REAL
0 * 0 is V42() real ext-real set
|.(G,seq).| is V42() real ext-real non negative Element of REAL
sqr (G,seq) 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,seq)) is V42() real ext-real Element of REAL
sqrt (Sum (sqr (G,seq))) is V42() real ext-real Element of REAL
||.(0. (G)).|| is V42() real ext-real Element of REAL
the normF of (G) is Relation-like Function-like non empty V14( the carrier of (G)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G),REAL:]
[: the carrier of (G),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G),REAL:] is V30() set
the normF of (G) . (0. (G)) is V42() real ext-real Element of REAL
the carrier of (G) is non empty set
seq is Element of the carrier of (G)
||.seq.|| is V42() real ext-real Element of REAL
the normF of (G) is Relation-like Function-like non empty V14( the carrier of (G)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G),REAL:]
[: the carrier of (G),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G),REAL:] is V30() set
the normF of (G) . seq is V42() real ext-real Element of REAL
0. (G) is V82((G)) Element of the carrier of (G)
the ZeroF of (G) is Element of the carrier of (G)
dom (G) is non empty 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
y0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)
x0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G
(G) . x0 is set
(G,x0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,x0) is non empty set
yy0 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
yy0 . x0 is set
(G,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 REAL (len G)
REAL (len G) is functional non empty FinSequence-membered FinSequenceSet of REAL
(len G) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len G } is set
|.(G,yy0).| is V42() real ext-real non negative Element of REAL
sqr (G,yy0) 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,yy0)) is V42() real ext-real Element of REAL
sqrt (Sum (sqr (G,yy0))) is V42() real ext-real Element of REAL
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
0* I is Relation-like NAT -defined REAL -valued Function-like V30() V37(I) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL I
REAL I is functional non empty FinSequence-membered FinSequenceSet of REAL
I -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = I } is set
I |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V30() V37(I) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of I -tuples_on REAL
Seg I is V30() V37(I) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
K106((Seg I),0) is Relation-like NAT -defined RAT -valued INT -valued Function-like V14( Seg I) quasi_total V30() FinSequence-like FinSubsequence-like complex-yielding V48() V49() V50() Cardinal-yielding countable Element of bool [:(Seg I),{0}:]
{0} is functional non empty trivial V37(1) with_common_domain V167() V168() V169() V170() V171() V172() set
[:(Seg I),{0}:] is Relation-like RAT -valued INT -valued complex-yielding V48() V49() V50() set
bool [:(Seg I),{0}:] is set
(G,yy0) . y0 is V42() real ext-real Element of REAL
j is Element of the carrier of (G,x0)
||.j.|| is V42() real ext-real non negative Element of REAL
the normF of (G,x0) is Relation-like Function-like non empty V14( the carrier of (G,x0)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G,x0),REAL:]
[: the carrier of (G,x0),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G,x0),REAL:] is V30() set
the normF of (G,x0) . j is V42() real ext-real Element of REAL
yy0 . y0 is Element of (G) . y0
(G) . y0 is non empty 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
0. (G,y0) is V82((G,y0)) Element of the carrier of (G,y0)
the carrier of (G,y0) is non empty set
the ZeroF of (G,y0) is Element of the carrier of (G,y0)
the carrier of (G) is non empty set
seq is Element of the carrier of (G)
||.seq.|| is V42() real ext-real Element of REAL
the normF of (G) is Relation-like Function-like non empty V14( the carrier of (G)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G),REAL:]
[: the carrier of (G),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G),REAL:] is V30() set
the normF of (G) . seq is V42() real ext-real Element of REAL
yy0 is Element of the carrier of (G)
seq + yy0 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
the addF of (G) . (seq,yy0) is Element of the carrier of (G)
||.(seq + yy0).|| is V42() real ext-real Element of REAL
the normF of (G) . (seq + yy0) is V42() real ext-real Element of REAL
||.yy0.|| is V42() real ext-real Element of REAL
the normF of (G) . yy0 is V42() real ext-real Element of REAL
||.seq.|| + ||.yy0.|| is V42() real ext-real Element of REAL
y0 is V42() real ext-real Element of REAL
y0 * seq is Element of the carrier of (G)
the Mult of (G) is Relation-like Function-like V14([:REAL, the carrier of (G):]) quasi_total Element of bool [:[:REAL, the carrier of (G):], the carrier of (G):]
[:REAL, the carrier of (G):] is Relation-like V30() set
[:[:REAL, the carrier of (G):], the carrier of (G):] is Relation-like V30() set
bool [:[:REAL, the carrier of (G):], the carrier of (G):] is V30() set
the Mult of (G) . (y0,seq) is set
||.(y0 * seq).|| is V42() real ext-real Element of REAL
the normF of (G) . (y0 * seq) is V42() real ext-real Element of REAL
abs y0 is V42() real ext-real Element of REAL
(abs y0) * ||.seq.|| is V42() real ext-real Element of REAL
i0 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
(G,i0) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
REAL (len G) is functional non empty FinSequence-membered FinSequenceSet of REAL
(len G) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len G } is set
|.(G,i0).| is V42() real ext-real non negative Element of REAL
sqr (G,i0) 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,i0)) is V42() real ext-real Element of REAL
sqrt (Sum (sqr (G,i0))) is V42() real ext-real Element of REAL
j is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
(G,j) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
(G,j) + (G,i0) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
|.((G,j) + (G,i0)).| is V42() real ext-real non negative Element of REAL
sqr ((G,j) + (G,i0)) 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,j) + (G,i0))) is V42() real ext-real Element of REAL
sqrt (Sum (sqr ((G,j) + (G,i0)))) is V42() real ext-real Element of REAL
|.(G,j).| is V42() real ext-real non negative Element of REAL
sqr (G,j) 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,j)) is V42() real ext-real Element of REAL
sqrt (Sum (sqr (G,j))) is V42() real ext-real Element of REAL
|.(G,j).| + |.(G,i0).| is V42() real ext-real non negative Element of REAL
seqi is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
(G,seqi) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
len (G,seqi) 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 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,seqi) is V37( len G) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
Seg I is V30() V37(I) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
x0 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
(G,x0) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
(abs y0) * (G,x0) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
seqi is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real countable set
(G,seqi) . seqi is V42() real ext-real Element of REAL
((abs y0) * (G,x0)) . seqi is V42() real ext-real Element of REAL
dom G is non empty 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
seqi is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G
(G) . seqi is set
(G,seqi) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,seqi) is non empty set
seqi . seqi is set
x0 . seqi is set
((G),REAL,(G)) . (y0,x0) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
i is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)
(((G),REAL,(G)) . (y0,x0)) . i is Element of (G) . i
(G) . i is non empty set
((G),REAL,(G),i) is Relation-like Function-like V14([:REAL,((G) . i):]) quasi_total Element of bool [:[:REAL,((G) . i):],((G) . i):]
[:REAL,((G) . i):] is Relation-like V30() set
[:[:REAL,((G) . i):],((G) . i):] is Relation-like V30() set
bool [:[:REAL,((G) . i):],((G) . i):] is V30() set
mx0 is Element of the carrier of (G,seqi)
((G),REAL,(G),i) . (y0,mx0) is set
seqimx0 is Element of the carrier of (G,seqi)
y0 * mx0 is Element of the carrier of (G,seqi)
the Mult of (G,seqi) is Relation-like Function-like V14([:REAL, the carrier of (G,seqi):]) quasi_total Element of bool [:[:REAL, the carrier of (G,seqi):], the carrier of (G,seqi):]
[:REAL, the carrier of (G,seqi):] is Relation-like V30() set
[:[:REAL, the carrier of (G,seqi):], the carrier of (G,seqi):] is Relation-like V30() set
bool [:[:REAL, the carrier of (G,seqi):], the carrier of (G,seqi):] is V30() set
the Mult of (G,seqi) . (y0,mx0) is set
||.seqimx0.|| is V42() real ext-real non negative Element of REAL
the normF of (G,seqi) is Relation-like Function-like non empty V14( the carrier of (G,seqi)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G,seqi),REAL:]
[: the carrier of (G,seqi),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G,seqi),REAL:] is V30() set
the normF of (G,seqi) . seqimx0 is V42() real ext-real Element of REAL
||.mx0.|| is V42() real ext-real non negative Element of REAL
the normF of (G,seqi) . mx0 is V42() real ext-real Element of REAL
(abs y0) * ||.mx0.|| is V42() real ext-real Element of REAL
(G,x0) . seqi is V42() real ext-real Element of REAL
(abs y0) * ((G,x0) . seqi) is V42() real ext-real Element of REAL
((abs y0) * (G,x0)) . seqi is V42() real ext-real Element of REAL
len ((abs y0) * (G,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
|.(G,seqi).| is V42() real ext-real non negative Element of REAL
sqr (G,seqi) 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,seqi)) is V42() real ext-real Element of REAL
sqrt (Sum (sqr (G,seqi))) is V42() real ext-real Element of REAL
|.((abs y0) * (G,x0)).| is V42() real ext-real non negative Element of REAL
sqr ((abs y0) * (G,x0)) is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable FinSequence of REAL
Sum (sqr ((abs y0) * (G,x0))) is V42() real ext-real Element of REAL
sqrt (Sum (sqr ((abs y0) * (G,x0)))) is V42() real ext-real Element of REAL
abs (abs y0) is V42() real ext-real Element of REAL
|.(G,x0).| is V42() real ext-real non negative Element of REAL
sqr (G,x0) 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,x0)) is V42() real ext-real Element of REAL
sqrt (Sum (sqr (G,x0))) is V42() real ext-real Element of REAL
(abs (abs y0)) * |.(G,x0).| is V42() real ext-real Element of REAL
seqi is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
(G,seqi) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
dom j is set
dom (G) is non empty 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
seqi 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,seqi) . seqi is V42() real ext-real Element of REAL
((G,j) + (G,i0)) . seqi is V42() real ext-real Element of REAL
dom seqi is set
len (G,seqi) 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,j) + (G,i0)) 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,seqi).| is V42() real ext-real non negative Element of REAL
sqr (G,seqi) 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,seqi)) is V42() real ext-real Element of REAL
sqrt (Sum (sqr (G,seqi))) is V42() real ext-real Element of REAL
G is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () () set
(G) is non empty strict NORMSTR
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
the Mult of (G) is Relation-like Function-like V14([:REAL, the carrier of (G):]) quasi_total Element of bool [:[:REAL, the carrier of (G):], the carrier of (G):]
[:REAL, the carrier of (G):] is Relation-like V30() set
[:[:REAL, the carrier of (G):], the carrier of (G):] is Relation-like V30() set
bool [:[:REAL, the carrier of (G):], the carrier of (G):] is V30() set
RLSStruct(# the carrier of (G), the ZeroF of (G), the addF of (G), the Mult of (G) #) is non empty strict RLSStruct
(G) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() 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
I is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () set
(I) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() RLSStruct
(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
(I) is Relation-like NAT -defined Function-like (I) -compatible Element of product (I)
(I) is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable BinOps of (I)
[:(I):] is Relation-like Function-like V14([:(product (I)),(product (I)):]) quasi_total Element of bool [:[:(product (I)),(product (I)):],(product (I)):]
[:(product (I)),(product (I)):] is Relation-like set
[:[:(product (I)),(product (I)):],(product (I)):] is Relation-like set
bool [:[:(product (I)),(product (I)):],(product (I)):] is set
(I) is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable ((I), REAL )
((I),REAL,(I)) is Relation-like Function-like V14([:REAL,(product (I)):]) quasi_total Element of bool [:[:REAL,(product (I)):],(product (I)):]
[:REAL,(product (I)):] is Relation-like V30() set
[:[:REAL,(product (I)):],(product (I)):] is Relation-like V30() set
bool [:[:REAL,(product (I)):],(product (I)):] is V30() set
RLSStruct(# (product (I)),(I),[:(I):],((I),REAL,(I)) #) is non empty strict RLSStruct
the carrier of (I) is non empty set
seq is Element of the carrier of (G)
1 * seq is Element of the carrier of (G)
the Mult of (G) . (1,seq) is set
yy0 is Element of the carrier of (I)
1 * yy0 is Element of the carrier of (I)
the Mult of (I) is Relation-like Function-like V14([:REAL, the carrier of (I):]) quasi_total Element of bool [:[:REAL, the carrier of (I):], the carrier of (I):]
[:REAL, the carrier of (I):] is Relation-like V30() set
[:[:REAL, the carrier of (I):], the carrier of (I):] is Relation-like V30() set
bool [:[:REAL, the carrier of (I):], the carrier of (I):] is V30() set
the Mult of (I) . (1,yy0) is set
seq is Element of the carrier of (G)
yy0 is Element of the carrier of (I)
- yy0 is Element of the carrier of (I)
y0 is Element of the carrier of (G)
seq + y0 is Element of the carrier of (G)
the addF of (G) . (seq,y0) is Element of the carrier of (G)
0. (G) is V82((G)) Element of the carrier of (G)
yy0 - yy0 is Element of the carrier of (I)
yy0 + (- yy0) is Element of the carrier of (I)
the addF of (I) is Relation-like Function-like V14([: the carrier of (I), the carrier of (I):]) quasi_total Element of bool [:[: the carrier of (I), the carrier of (I):], the carrier of (I):]
[: the carrier of (I), the carrier of (I):] is Relation-like set
[:[: the carrier of (I), the carrier of (I):], the carrier of (I):] is Relation-like set
bool [:[: the carrier of (I), the carrier of (I):], the carrier of (I):] is set
the addF of (I) . (yy0,(- yy0)) is Element of the carrier of (I)
0. (I) is V82((I)) Element of the carrier of (I)
the ZeroF of (I) is Element of the carrier of (I)
yy0 is Element of the carrier of (G)
y0 is Element of the carrier of (G)
yy0 + y0 is Element of the carrier of (G)
the addF of (G) . (yy0,y0) is Element of the carrier of (G)
seq is V42() real ext-real set
seq * (yy0 + y0) is Element of the carrier of (G)
the Mult of (G) . (seq,(yy0 + y0)) is set
x0 is Element of the carrier of (I)
j is Element of the carrier of (I)
x0 + j is Element of the carrier of (I)
the addF of (I) is Relation-like Function-like V14([: the carrier of (I), the carrier of (I):]) quasi_total Element of bool [:[: the carrier of (I), the carrier of (I):], the carrier of (I):]
[: the carrier of (I), the carrier of (I):] is Relation-like set
[:[: the carrier of (I), the carrier of (I):], the carrier of (I):] is Relation-like set
bool [:[: the carrier of (I), the carrier of (I):], the carrier of (I):] is set
the addF of (I) . (x0,j) is Element of the carrier of (I)
seq * (x0 + j) is Element of the carrier of (I)
the Mult of (I) . (seq,(x0 + j)) is set
seq * x0 is Element of the carrier of (I)
the Mult of (I) . (seq,x0) is set
seq * j is Element of the carrier of (I)
the Mult of (I) . (seq,j) is set
(seq * x0) + (seq * j) is Element of the carrier of (I)
the addF of (I) . ((seq * x0),(seq * j)) is Element of the carrier of (I)
seq * yy0 is Element of the carrier of (G)
the Mult of (G) . (seq,yy0) is set
seq * y0 is Element of the carrier of (G)
the Mult of (G) . (seq,y0) is set
(seq * yy0) + (seq * y0) is Element of the carrier of (G)
the addF of (G) . ((seq * yy0),(seq * y0)) is Element of the carrier of (G)
y0 is Element of the carrier of (G)
seq is V42() real ext-real set
yy0 is V42() real ext-real set
seq * yy0 is V42() real ext-real set
(seq * yy0) * y0 is Element of the carrier of (G)
the Mult of (G) . ((seq * yy0),y0) is set
x0 is Element of the carrier of (I)
(seq * yy0) * x0 is Element of the carrier of (I)
the Mult of (I) . ((seq * yy0),x0) is set
yy0 * x0 is Element of the carrier of (I)
the Mult of (I) . (yy0,x0) is set
seq * (yy0 * x0) is Element of the carrier of (I)
the Mult of (I) . (seq,(yy0 * x0)) is set
yy0 * y0 is Element of the carrier of (G)
the Mult of (G) . (yy0,y0) is set
seq * (yy0 * y0) is Element of the carrier of (G)
the Mult of (G) . (seq,(yy0 * y0)) is set
y0 is Element of the carrier of (G)
seq is V42() real ext-real set
yy0 is V42() real ext-real set
seq + yy0 is V42() real ext-real set
(seq + yy0) * y0 is Element of the carrier of (G)
the Mult of (G) . ((seq + yy0),y0) is set
x0 is Element of the carrier of (I)
(seq + yy0) * x0 is Element of the carrier of (I)
the Mult of (I) . ((seq + yy0),x0) is set
seq * x0 is Element of the carrier of (I)
the Mult of (I) . (seq,x0) is set
yy0 * x0 is Element of the carrier of (I)
the Mult of (I) . (yy0,x0) is set
(seq * x0) + (yy0 * x0) is Element of the carrier of (I)
the addF of (I) . ((seq * x0),(yy0 * x0)) is Element of the carrier of (I)
seq * y0 is Element of the carrier of (G)
the Mult of (G) . (seq,y0) is set
yy0 * y0 is Element of the carrier of (G)
the Mult of (G) . (yy0,y0) is set
(seq * y0) + (yy0 * y0) is Element of the carrier of (G)
the addF of (G) . ((seq * y0),(yy0 * y0)) is Element of the carrier of (G)
seq is Element of the carrier of (G)
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)
y0 is Element of the carrier of (G)
(seq + yy0) + y0 is Element of the carrier of (G)
the addF of (G) . ((seq + yy0),y0) is Element of the carrier of (G)
yy0 + y0 is Element of the carrier of (G)
the addF of (G) . (yy0,y0) is Element of the carrier of (G)
seq + (yy0 + y0) is Element of the carrier of (G)
the addF of (G) . (seq,(yy0 + y0)) is Element of the carrier of (G)
x0 is Element of the carrier of (I)
j is Element of the carrier of (I)
x0 + j is Element of the carrier of (I)
the addF of (I) . (x0,j) is Element of the carrier of (I)
i0 is Element of the carrier of (I)
(x0 + j) + i0 is Element of the carrier of (I)
the addF of (I) . ((x0 + j),i0) is Element of the carrier of (I)
j + i0 is Element of the carrier of (I)
the addF of (I) . (j,i0) is Element of the carrier of (I)
x0 + (j + i0) is Element of the carrier of (I)
the addF of (I) . (x0,(j + i0)) is Element of the carrier of (I)
seq is Element of the carrier of (G)
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)
yy0 + seq is Element of the carrier of (G)
the addF of (G) . (yy0,seq) is Element of the carrier of (G)
y0 is Element of the carrier of (I)
x0 is Element of the carrier of (I)
y0 + x0 is Element of the carrier of (I)
the addF of (I) . (y0,x0) is Element of the carrier of (I)
x0 + y0 is Element of the carrier of (I)
the addF of (I) . (x0,y0) is Element of the carrier of (I)
seq is Element of the carrier of (G)
0. (G) is V82((G)) Element of the carrier of (G)
seq + (0. (G)) is Element of the carrier of (G)
the addF of (G) . (seq,(0. (G))) is Element of the carrier of (G)
yy0 is Element of the carrier of (I)
0. (I) is V82((I)) Element of the carrier of (I)
the ZeroF of (I) is Element of the carrier of (I)
yy0 + (0. (I)) is Element of the carrier of (I)
the addF of (I) . (yy0,(0. (I))) is Element of the carrier of (I)
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
(G) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive strict RealNormSpace-like NORMSTR
the carrier of (G) is non empty 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
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() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,I) is non empty set
seq is Element of the carrier of (G)
||.seq.|| is V42() real ext-real non negative Element of REAL
the normF of (G) is Relation-like Function-like non empty V14( the carrier of (G)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G),REAL:]
[: the carrier of (G),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G),REAL:] is V30() set
the normF of (G) . seq is V42() real ext-real Element of REAL
yy0 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
yy0 . I is set
y0 is Element of the carrier of (G,I)
||.y0.|| is V42() real ext-real non negative Element of REAL
the normF of (G,I) is Relation-like Function-like non empty V14( the carrier of (G,I)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G,I),REAL:]
[: the carrier of (G,I),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G,I),REAL:] is V30() set
the normF of (G,I) . y0 is V42() real ext-real Element of REAL
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
(G,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 REAL (len G)
REAL (len G) is functional non empty FinSequence-membered FinSequenceSet of REAL
(len G) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len G } is set
(G,yy0) . I is V42() real ext-real Element of REAL
((G,yy0) . I) ^2 is V42() real ext-real Element of REAL
((G,yy0) . I) * ((G,yy0) . I) is V42() real ext-real set
sqr (G,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
(sqr (G,yy0)) . I is V42() real ext-real Element of REAL
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
Seg x0 is V30() V37(x0) countable V167() V168() V169() V170() V171() V172() Element of bool 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
(sqr (G,yy0)) . j is V42() real ext-real Element of REAL
(G,yy0) . j is V42() real ext-real Element of REAL
((G,yy0) . j) ^2 is V42() real ext-real Element of REAL
((G,yy0) . j) * ((G,yy0) . j) is V42() real ext-real set
Sum (sqr (G,yy0)) is V42() real ext-real Element of REAL
sqrt ((sqr (G,yy0)) . I) is V42() real ext-real Element of REAL
|.(G,yy0).| is V42() real ext-real non negative Element of REAL
sqr (G,yy0) 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,yy0)) is V42() real ext-real Element of REAL
sqrt (Sum (sqr (G,yy0))) is V42() real ext-real Element of REAL
G is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR
the carrier of G is non empty set
[:NAT, the carrier of G:] is Relation-like V30() set
bool [:NAT, the carrier of G:] is V30() set
I is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of G:]
lim I is Element of the carrier of G
seq is Element of the carrier of G
I - seq is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of G:]
||.(I - seq).|| is Relation-like Function-like non empty V14( NAT ) quasi_total complex-yielding V48() V49() Element of bool [:NAT,REAL:]
lim ||.(I - seq).|| is V42() real ext-real Element of REAL
yy0 is V42() real ext-real Element of REAL
y0 is V42() real ext-real set
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
i0 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 - seq).|| . i0 is V42() real ext-real Element of REAL
(||.(I - seq).|| . i0) - 0 is V42() real ext-real Element of REAL
abs ((||.(I - seq).|| . i0) - 0) is V42() real ext-real Element of REAL
(I - seq) . i0 is Element of the carrier of G
||.((I - seq) . i0).|| is V42() real ext-real non negative Element of REAL
the normF of G is Relation-like Function-like non empty V14( the carrier of G) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of G,REAL:]
[: the carrier of G,REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of G,REAL:] is V30() set
the normF of G . ((I - seq) . i0) is V42() real ext-real Element of REAL
abs ||.((I - seq) . i0).|| is V42() real ext-real Element of REAL
I . i0 is Element of the carrier of G
(I . i0) - seq is Element of the carrier of G
- seq is Element of the carrier of G
(I . i0) + (- seq) 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
the addF of G . ((I . i0),(- seq)) is Element of the carrier of G
||.((I . i0) - seq).|| is V42() real ext-real non negative Element of REAL
the normF of G . ((I . i0) - seq) is V42() real ext-real Element of REAL
abs ||.((I . i0) - seq).|| is V42() real ext-real Element of REAL
i0 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 . i0 is Element of the carrier of G
(I . i0) - seq is Element of the carrier of G
(I . i0) + (- seq) is Element of the carrier of G
the addF of G . ((I . i0),(- seq)) is Element of the carrier of G
||.((I . i0) - seq).|| is V42() real ext-real non negative Element of REAL
the normF of G . ((I . i0) - seq) is V42() real ext-real Element of REAL
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
(G) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive strict RealNormSpace-like NORMSTR
the carrier of (G) is non empty 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
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() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,I) is non empty set
seq is Element of the carrier of (G)
yy0 is Element of the carrier of (G)
yy0 - seq is Element of the carrier of (G)
- seq is Element of the carrier of (G)
yy0 + (- seq) 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
the addF of (G) . (yy0,(- seq)) is Element of the carrier of (G)
||.(yy0 - seq).|| is V42() real ext-real non negative Element of REAL
the normF of (G) is Relation-like Function-like non empty V14( the carrier of (G)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G),REAL:]
[: the carrier of (G),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G),REAL:] is V30() set
the normF of (G) . (yy0 - seq) is V42() real ext-real Element of REAL
y0 is Element of the carrier of (G,I)
x0 is Element of the carrier of (G,I)
x0 - y0 is Element of the carrier of (G,I)
- y0 is Element of the carrier of (G,I)
x0 + (- y0) 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) . (x0,(- y0)) is Element of the carrier of (G,I)
||.(x0 - y0).|| is V42() real ext-real non negative Element of REAL
the normF of (G,I) is Relation-like Function-like non empty V14( the carrier of (G,I)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G,I),REAL:]
[: the carrier of (G,I),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G,I),REAL:] is V30() set
the normF of (G,I) . (x0 - y0) is V42() real ext-real Element of REAL
j is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
j . I is set
i0 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
i0 . I is 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
(G) is Relation-like Function-like non empty V14( product (G)) quasi_total complex-yielding V48() V49() Element of bool [:(product (G)),REAL:]
[:(product (G)),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [:(product (G)),REAL:] is V30() set
NORMSTR(# (product (G)),(G),[:(G):],((G),REAL,(G)),(G) #) is strict NORMSTR
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
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
(- 1) * seq is Element of the carrier of (G)
the Mult of (G) is Relation-like Function-like V14([:REAL, the carrier of (G):]) quasi_total Element of bool [:[:REAL, the carrier of (G):], the carrier of (G):]
[:REAL, the carrier of (G):] is Relation-like V30() set
[:[:REAL, the carrier of (G):], the carrier of (G):] is Relation-like V30() set
bool [:[:REAL, the carrier of (G):], the carrier of (G):] is V30() set
the Mult of (G) . ((- 1),seq) is set
seqi is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
seqi . I is set
seqi is Element of the carrier of (G,I)
(- 1) * seqi 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),seqi) is set
seqimx0 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
seqimx0 . I is set
seqi is Element of the carrier of (G,I)
i is Element of the carrier of (G,I)
seqi + i is Element of the carrier of (G,I)
the addF of (G,I) . (seqi,i) is Element of the carrier of (G,I)
- seqi is Element of the carrier of (G,I)
seqi + (- seqi) is Element of the carrier of (G,I)
the addF of (G,I) . (seqi,(- seqi)) is Element of the carrier of (G,I)
G is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () () set
(G) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive strict RealNormSpace-like NORMSTR
the carrier of (G) is non empty set
[:NAT, the carrier of (G):] is Relation-like V30() set
bool [:NAT, the carrier of (G):] is V30() 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
I is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G):]
lim I is Element of the carrier of (G)
seq is Element of the carrier of (G)
yy0 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
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() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,y0) is non empty set
[:NAT, the carrier of (G,y0):] is Relation-like V30() set
bool [:NAT, the carrier of (G,y0):] is V30() set
yy0 . y0 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
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
(G) . y0 is set
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 Element of the carrier of (G)
(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
(G) is Relation-like Function-like non empty V14( product (G)) quasi_total complex-yielding V48() V49() Element of bool [:(product (G)),REAL:]
[:(product (G)),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [:(product (G)),REAL:] is V30() set
NORMSTR(# (product (G)),(G),[:(G):],((G),REAL,(G)),(G) #) is strict NORMSTR
i0 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
i0 . y0 is set
j is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,y0):]
j is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,y0):]
lim j is Element of the carrier of (G,y0)
x0 is Element of the carrier of (G,y0)
i0 is V42() real ext-real Element of REAL
seqi 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
seqi 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 . seqi is Element of the carrier of (G)
(I . seqi) - seq is Element of the carrier of (G)
- seq is Element of the carrier of (G)
(I . seqi) + (- seq) 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
the addF of (G) . ((I . seqi),(- seq)) is Element of the carrier of (G)
||.((I . seqi) - seq).|| is V42() real ext-real non negative Element of REAL
the normF of (G) is Relation-like Function-like non empty V14( the carrier of (G)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G),REAL:]
[: the carrier of (G),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G),REAL:] is V30() set
the normF of (G) . ((I . seqi) - seq) is V42() real ext-real Element of REAL
j . seqi is Element of the carrier of (G,y0)
(j . seqi) - x0 is Element of the carrier of (G,y0)
- x0 is Element of the carrier of (G,y0)
(j . seqi) + (- x0) is Element of the carrier of (G,y0)
the addF of (G,y0) is Relation-like Function-like V14([: the carrier of (G,y0), the carrier of (G,y0):]) quasi_total Element of bool [:[: the carrier of (G,y0), the carrier of (G,y0):], the carrier of (G,y0):]
[: the carrier of (G,y0), the carrier of (G,y0):] is Relation-like set
[:[: the carrier of (G,y0), the carrier of (G,y0):], the carrier of (G,y0):] is Relation-like set
bool [:[: the carrier of (G,y0), the carrier of (G,y0):], the carrier of (G,y0):] is set
the addF of (G,y0) . ((j . seqi),(- x0)) is Element of the carrier of (G,y0)
||.((j . seqi) - x0).|| is V42() real ext-real non negative Element of REAL
the normF of (G,y0) is Relation-like Function-like non empty V14( the carrier of (G,y0)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G,y0),REAL:]
[: the carrier of (G,y0),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G,y0),REAL:] is V30() set
the normF of (G,y0) . ((j . seqi) - x0) is V42() real ext-real Element of REAL
seqi is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
seqi . y0 is set
i0 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 . i0 is Element of the carrier of (G)
j . i0 is Element of the carrier of (G,y0)
G is Relation-like NAT -defined Function-like non empty V30() FinSequence-like FinSubsequence-like countable () () set
(G) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive strict RealNormSpace-like NORMSTR
the carrier of (G) is non empty set
[:NAT, the carrier of (G):] is Relation-like V30() set
bool [:NAT, the carrier of (G):] is V30() 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
I is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G):]
lim I is Element of the carrier of (G)
seq is Element of the carrier of (G)
yy0 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
Funcs (NAT,REAL) is functional non empty FUNCTION_DOMAIN of NAT , REAL
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() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,y0) is non empty set
[:NAT, the carrier of (G,y0):] is Relation-like V30() set
bool [:NAT, the carrier of (G,y0):] is V30() set
yy0 . y0 is set
x0 is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,y0):]
lim x0 is Element of the carrier of (G,y0)
x0 - (lim x0) is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,y0):]
||.(x0 - (lim x0)).|| is Relation-like Function-like non empty V14( NAT ) quasi_total complex-yielding V48() V49() Element of bool [:NAT,REAL:]
lim ||.(x0 - (lim x0)).|| is V42() real ext-real Element of REAL
[:(dom G),(Funcs (NAT,REAL)):] is Relation-like set
bool [:(dom G),(Funcs (NAT,REAL)):] is set
y0 is Relation-like Function-like non empty V14( dom G) quasi_total Element of bool [:(dom G),(Funcs (NAT,REAL)):]
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
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
REAL x0 is functional non empty FinSequence-membered FinSequenceSet of REAL
x0 -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = x0 } is set
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
Seg x0 is V30() V37(x0) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
i0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real countable set
seqi is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G
y0 . seqi is Relation-like Function-like Element of Funcs (NAT,REAL)
(y0 . seqi) . j is set
i0 is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like countable set
dom i0 is countable V167() V168() V169() V170() V171() V172() Element of bool NAT
seqi is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real countable set
i0 . seqi is set
seqi is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G
y0 . seqi is Relation-like Function-like Element of Funcs (NAT,REAL)
(y0 . seqi) . j is set
seqi is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable FinSequence of REAL
len seqi 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 seqi) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len seqi } is set
seqi is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G
seqi is Relation-like NAT -defined REAL -valued Function-like V30() V37(x0) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL x0
seqi . seqi is V42() real ext-real Element of REAL
y0 . seqi is Relation-like Function-like Element of Funcs (NAT,REAL)
(y0 . seqi) . j is set
i is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G
y0 . i is Relation-like Function-like Element of Funcs (NAT,REAL)
(y0 . i) . j is set
[:NAT,(REAL x0):] is Relation-like V30() set
bool [:NAT,(REAL x0):] is V30() set
j is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(REAL x0):]
i0 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 x0 is V30() V37(x0) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
seqi is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G
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 left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,seqi) is non empty set
[:NAT, the carrier of (G,seqi):] is Relation-like V30() set
bool [:NAT, the carrier of (G,seqi):] is V30() set
y0 . seqi is Relation-like Function-like Element of Funcs (NAT,REAL)
seqi is Relation-like Function-like non empty V14( NAT ) quasi_total complex-yielding V48() V49() Element of bool [:NAT,REAL:]
i is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,seqi):]
lim seqi is V42() real ext-real Element of REAL
lim i is Element of the carrier of (G,seqi)
i - (lim i) is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,seqi):]
||.(i - (lim i)).|| is Relation-like Function-like non empty V14( NAT ) quasi_total complex-yielding V48() V49() Element of bool [:NAT,REAL:]
seqimx0 is Relation-like Function-like non empty V14( NAT ) quasi_total complex-yielding V48() V49() Element of bool [:NAT,REAL:]
mx0 is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,seqi):]
lim seqimx0 is V42() real ext-real Element of REAL
0* x0 is Relation-like NAT -defined REAL -valued Function-like V30() V37(x0) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL x0
x0 |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V30() V37(x0) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of x0 -tuples_on REAL
K106((Seg x0),0) is Relation-like NAT -defined RAT -valued INT -valued Function-like V14( Seg x0) quasi_total V30() FinSequence-like FinSubsequence-like complex-yielding V48() V49() V50() Cardinal-yielding countable Element of bool [:(Seg x0),{0}:]
{0} is functional non empty trivial V37(1) with_common_domain V167() V168() V169() V170() V171() V172() set
[:(Seg x0),{0}:] is Relation-like RAT -valued INT -valued complex-yielding V48() V49() V50() set
bool [:(Seg x0),{0}:] is set
(0* x0) . seqi is V42() real ext-real Element of REAL
lim mx0 is Element of the carrier of (G,seqi)
mx0 - (lim mx0) is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,seqi):]
||.(mx0 - (lim mx0)).|| is Relation-like Function-like non empty V14( NAT ) quasi_total complex-yielding V48() V49() Element of bool [:NAT,REAL:]
k 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
seqimx0 . k is V42() real ext-real Element of REAL
j . k is Relation-like NAT -defined REAL -valued Function-like V30() V37(x0) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL x0
(j . k) . i0 is V42() real ext-real Element of REAL
k0 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 . k0 is Element of the carrier of (G)
mx0 . k0 is Element of the carrier of (G,seqi)
REAL-NS x0 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive strict RealNormSpace-like complete NORMSTR
the carrier of (REAL-NS x0) is non empty set
[:NAT, the carrier of (REAL-NS x0):] is Relation-like V30() set
bool [:NAT, the carrier of (REAL-NS x0):] is V30() set
i0 is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (REAL-NS x0):]
seqi is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (REAL-NS x0):]
seqi is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(REAL x0):]
seqi 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
(0* x0) . seqi is V42() real ext-real Element of REAL
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() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,i) is non empty set
[:NAT, the carrier of (G,i):] is Relation-like V30() set
bool [:NAT, the carrier of (G,i):] is V30() set
seqimx0 is Relation-like Function-like non empty V14( NAT ) quasi_total complex-yielding V48() V49() Element of bool [:NAT,REAL:]
mx0 is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,i):]
lim seqimx0 is V42() real ext-real Element of REAL
(0* x0) . i is V42() real ext-real Element of REAL
lim mx0 is Element of the carrier of (G,i)
mx0 - (lim mx0) is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,i):]
||.(mx0 - (lim mx0)).|| is Relation-like Function-like non empty V14( NAT ) quasi_total complex-yielding V48() V49() Element of bool [:NAT,REAL:]
(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
(G) is Relation-like Function-like non empty V14( product (G)) quasi_total complex-yielding V48() V49() Element of bool [:(product (G)),REAL:]
[:(product (G)),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [:(product (G)),REAL:] is V30() set
NORMSTR(# (product (G)),(G),[:(G):],((G),REAL,(G)),(G) #) is strict NORMSTR
seqi is set
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
I . i is Element of the carrier of (G)
(I . i) - seq is Element of the carrier of (G)
- seq is Element of the carrier of (G)
(I . i) + (- seq) 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
the addF of (G) . ((I . i),(- seq)) is Element of the carrier of (G)
k is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real countable set
seqimx0 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
(G,seqimx0) is Relation-like NAT -defined REAL -valued Function-like V30() V37( len G) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL (len G)
REAL (len G) is functional non empty FinSequence-membered FinSequenceSet of REAL
(len G) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V30() FinSequence-like FinSubsequence-like countable Element of REAL * : len b1 = len G } is set
dom (G,seqimx0) is V37( len G) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
len (G,seqimx0) 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
k1 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G
(G,k1) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,k1) is non empty set
[:NAT, the carrier of (G,k1):] is Relation-like V30() set
bool [:NAT, the carrier of (G,k1):] is V30() set
rseqk1i is Relation-like Function-like non empty V14( NAT ) quasi_total complex-yielding V48() V49() Element of bool [:NAT,REAL:]
seqk1i is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,k1):]
lim rseqk1i is V42() real ext-real Element of REAL
(0* x0) . k1 is V42() real ext-real Element of REAL
lim seqk1i is Element of the carrier of (G,k1)
seqk1i - (lim seqk1i) is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,k1):]
||.(seqk1i - (lim seqk1i)).|| is Relation-like Function-like non empty V14( NAT ) quasi_total complex-yielding V48() V49() Element of bool [:NAT,REAL:]
k0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G
(G,k0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,k0) is non empty set
[:NAT, the carrier of (G,k0):] is Relation-like V30() set
bool [:NAT, the carrier of (G,k0):] is V30() set
yy0 . k0 is set
seqk0 is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,k0):]
lim seqk0 is Element of the carrier of (G,k0)
seqk0 . i is Element of the carrier of (G,k0)
x is set
m 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 . m is Element of the carrier of (G)
seqk1i . m is Element of the carrier of (G,k1)
seqk0 . m is Element of the carrier of (G,k0)
seqk1i . x is set
seqk0 . x is set
c23 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
c23 . k1 is set
c24 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
c24 . k0 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
(- 1) * seq is Element of the carrier of (G)
the Mult of (G) is Relation-like Function-like V14([:REAL, the carrier of (G):]) quasi_total Element of bool [:[:REAL, the carrier of (G):], the carrier of (G):]
[:REAL, the carrier of (G):] is Relation-like V30() set
[:[:REAL, the carrier of (G):], the carrier of (G):] is Relation-like V30() set
bool [:[:REAL, the carrier of (G):], the carrier of (G):] is V30() set
the Mult of (G) . ((- 1),seq) is set
mx0 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
mx0 . k0 is set
(- 1) * (lim seqk0) is Element of the carrier of (G,k0)
the Mult of (G,k0) is Relation-like Function-like V14([:REAL, the carrier of (G,k0):]) quasi_total Element of bool [:[:REAL, the carrier of (G,k0):], the carrier of (G,k0):]
[:REAL, the carrier of (G,k0):] is Relation-like V30() set
[:[:REAL, the carrier of (G,k0):], the carrier of (G,k0):] is Relation-like V30() set
bool [:[:REAL, the carrier of (G,k0):], the carrier of (G,k0):] is V30() set
the Mult of (G,k0) . ((- 1),(lim seqk0)) is set
- (lim seqk0) is Element of the carrier of (G,k0)
seqimx0 . k0 is set
(seqk0 . i) - (lim seqk0) is Element of the carrier of (G,k0)
(seqk0 . i) + (- (lim seqk0)) is Element of the carrier of (G,k0)
the addF of (G,k0) is Relation-like Function-like V14([: the carrier of (G,k0), the carrier of (G,k0):]) quasi_total Element of bool [:[: the carrier of (G,k0), the carrier of (G,k0):], the carrier of (G,k0):]
[: the carrier of (G,k0), the carrier of (G,k0):] is Relation-like set
[:[: the carrier of (G,k0), the carrier of (G,k0):], the carrier of (G,k0):] is Relation-like set
bool [:[: the carrier of (G,k0), the carrier of (G,k0):], the carrier of (G,k0):] is set
the addF of (G,k0) . ((seqk0 . i),(- (lim seqk0))) is Element of the carrier of (G,k0)
x is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
x . k0 is set
(G,seqimx0) . k is V42() real ext-real Element of REAL
the normF of (G,k0) is Relation-like Function-like non empty V14( the carrier of (G,k0)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G,k0),REAL:]
[: the carrier of (G,k0),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G,k0),REAL:] is V30() set
the normF of (G,k0) . (seqimx0 . k0) is V42() real ext-real Element of REAL
seqk0 - (lim seqk0) is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,k0):]
(seqk0 - (lim seqk0)) . i is Element of the carrier of (G,k0)
||.((seqk0 - (lim seqk0)) . i).|| is V42() real ext-real non negative Element of REAL
the normF of (G,k0) . ((seqk0 - (lim seqk0)) . i) is V42() real ext-real Element of REAL
||.(seqk1i - (lim seqk1i)).|| . i is V42() real ext-real Element of REAL
seqi . i is Relation-like NAT -defined REAL -valued Function-like V30() V37(x0) FinSequence-like FinSubsequence-like complex-yielding V48() V49() countable Element of REAL x0
(seqi . i) . k is V42() real ext-real Element of REAL
len (seqi . 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
dom (seqi . i) is V37(x0) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
0. (REAL-NS x0) is V82( REAL-NS x0) Element of the carrier of (REAL-NS x0)
the ZeroF of (REAL-NS x0) is Element of the carrier of (REAL-NS x0)
seqi - (0. (REAL-NS x0)) is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (REAL-NS x0):]
||.(seqi - (0. (REAL-NS x0))).|| is Relation-like Function-like non empty V14( NAT ) quasi_total complex-yielding V48() V49() Element of bool [:NAT,REAL:]
||.(seqi - (0. (REAL-NS x0))).|| . seqi is V42() real ext-real Element of REAL
(seqi - (0. (REAL-NS x0))) . i is Element of the carrier of (REAL-NS x0)
||.((seqi - (0. (REAL-NS x0))) . i).|| is V42() real ext-real non negative Element of REAL
the normF of (REAL-NS x0) is Relation-like Function-like non empty V14( the carrier of (REAL-NS x0)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (REAL-NS x0),REAL:]
[: the carrier of (REAL-NS x0),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (REAL-NS x0),REAL:] is V30() set
the normF of (REAL-NS x0) . ((seqi - (0. (REAL-NS x0))) . i) is V42() real ext-real Element of REAL
seqi . i is Element of the carrier of (REAL-NS x0)
(seqi . i) - (0. (REAL-NS x0)) is Element of the carrier of (REAL-NS x0)
- (0. (REAL-NS x0)) is Element of the carrier of (REAL-NS x0)
(seqi . i) + (- (0. (REAL-NS x0))) is Element of the carrier of (REAL-NS x0)
the addF of (REAL-NS x0) is Relation-like Function-like V14([: the carrier of (REAL-NS x0), the carrier of (REAL-NS x0):]) quasi_total Element of bool [:[: the carrier of (REAL-NS x0), the carrier of (REAL-NS x0):], the carrier of (REAL-NS x0):]
[: the carrier of (REAL-NS x0), the carrier of (REAL-NS x0):] is Relation-like set
[:[: the carrier of (REAL-NS x0), the carrier of (REAL-NS x0):], the carrier of (REAL-NS x0):] is Relation-like set
bool [:[: the carrier of (REAL-NS x0), the carrier of (REAL-NS x0):], the carrier of (REAL-NS x0):] is set
the addF of (REAL-NS x0) . ((seqi . i),(- (0. (REAL-NS x0)))) is Element of the carrier of (REAL-NS x0)
||.((seqi . i) - (0. (REAL-NS x0))).|| is V42() real ext-real non negative Element of REAL
the normF of (REAL-NS x0) . ((seqi . i) - (0. (REAL-NS x0))) is V42() real ext-real Element of REAL
||.(seqi . i).|| is V42() real ext-real non negative Element of REAL
the normF of (REAL-NS x0) . (seqi . i) is V42() real ext-real Element of REAL
|.(seqi . i).| is V42() real ext-real non negative Element of REAL
sqr (seqi . 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 (seqi . i)) is V42() real ext-real Element of REAL
sqrt (Sum (sqr (seqi . i))) is V42() real ext-real Element of REAL
||.((I . i) - seq).|| is V42() real ext-real non negative Element of REAL
the normF of (G) is Relation-like Function-like non empty V14( the carrier of (G)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G),REAL:]
[: the carrier of (G),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G),REAL:] is V30() set
the normF of (G) . ((I . i) - seq) is V42() real ext-real Element of REAL
I - seq is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G):]
(I - seq) . i is Element of the carrier of (G)
||.((I - seq) . i).|| is V42() real ext-real non negative Element of REAL
the normF of (G) . ((I - seq) . i) is V42() real ext-real Element of REAL
||.(I - seq).|| is Relation-like Function-like non empty V14( NAT ) quasi_total complex-yielding V48() V49() Element of bool [:NAT,REAL:]
||.(I - seq).|| . seqi is V42() real ext-real Element of REAL
lim seqi is Element of the carrier of (REAL-NS x0)
lim ||.(I - seq).|| is V42() real ext-real Element of REAL
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
(G) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive strict RealNormSpace-like NORMSTR
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
(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
(G) is Relation-like Function-like non empty V14( product (G)) quasi_total complex-yielding V48() V49() Element of bool [:(product (G)),REAL:]
[:(product (G)),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [:(product (G)),REAL:] is V30() set
NORMSTR(# (product (G)),(G),[:(G):],((G),REAL,(G)),(G) #) is strict NORMSTR
the carrier of (G) is non empty set
[:NAT, the carrier of (G):] is Relation-like V30() set
bool [:NAT, the carrier of (G):] is V30() set
seq is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G):]
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 I is V30() V37(I) 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 countable 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() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,y0) is non empty set
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
seq . x0 is Element of the carrier of (G)
j is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
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
j . y0 is set
(G) . y0 is set
[:NAT, the carrier of (G,y0):] is Relation-like V30() set
bool [:NAT, the carrier of (G,y0):] is V30() set
x0 is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,y0):]
x0 is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,y0):]
lim x0 is Element of the carrier of (G,y0)
j is V42() real ext-real Element of REAL
i0 is V42() real ext-real Element of REAL
seqi 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
seqi 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
seqi 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 . seqi is Element of the carrier of (G)
seq . seqi is Element of the carrier of (G)
(seq . seqi) - (seq . seqi) is Element of the carrier of (G)
- (seq . seqi) is Element of the carrier of (G)
(seq . seqi) + (- (seq . seqi)) 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
the addF of (G) . ((seq . seqi),(- (seq . seqi))) is Element of the carrier of (G)
||.((seq . seqi) - (seq . seqi)).|| is V42() real ext-real non negative Element of REAL
the normF of (G) is Relation-like Function-like non empty V14( the carrier of (G)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G),REAL:]
[: the carrier of (G),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G),REAL:] is V30() set
the normF of (G) . ((seq . seqi) - (seq . seqi)) is V42() real ext-real Element of REAL
x0 . seqi is Element of the carrier of (G,y0)
x0 . seqi is Element of the carrier of (G,y0)
(x0 . seqi) - (x0 . seqi) is Element of the carrier of (G,y0)
- (x0 . seqi) is Element of the carrier of (G,y0)
(x0 . seqi) + (- (x0 . seqi)) is Element of the carrier of (G,y0)
the addF of (G,y0) is Relation-like Function-like V14([: the carrier of (G,y0), the carrier of (G,y0):]) quasi_total Element of bool [:[: the carrier of (G,y0), the carrier of (G,y0):], the carrier of (G,y0):]
[: the carrier of (G,y0), the carrier of (G,y0):] is Relation-like set
[:[: the carrier of (G,y0), the carrier of (G,y0):], the carrier of (G,y0):] is Relation-like set
bool [:[: the carrier of (G,y0), the carrier of (G,y0):], the carrier of (G,y0):] is set
the addF of (G,y0) . ((x0 . seqi),(- (x0 . seqi))) is Element of the carrier of (G,y0)
||.((x0 . seqi) - (x0 . seqi)).|| is V42() real ext-real non negative Element of REAL
the normF of (G,y0) is Relation-like Function-like non empty V14( the carrier of (G,y0)) quasi_total complex-yielding V48() V49() Element of bool [: the carrier of (G,y0),REAL:]
[: the carrier of (G,y0),REAL:] is Relation-like V30() complex-yielding V48() V49() set
bool [: the carrier of (G,y0),REAL:] is V30() set
the normF of (G,y0) . ((x0 . seqi) - (x0 . seqi)) is V42() real ext-real Element of REAL
i is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
i . y0 is set
seqimx0 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
seqimx0 . y0 is 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
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
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
y0 is set
dom (G) is non empty countable V167() V168() V169() V170() V171() V172() Element of bool NAT
x0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom (G)
j is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G
i0 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 . i0 is set
yy0 . j is set
(G,j) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,j) is non empty 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 left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,seqi) is non empty set
[:NAT, the carrier of (G,seqi):] is Relation-like V30() set
bool [:NAT, the carrier of (G,seqi):] is V30() set
seqi is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,seqi):]
lim seqi is Element of the carrier of (G,seqi)
yy0 . y0 is set
(G) . y0 is set
Seg (len (G)) is non empty V30() V37( len (G)) countable V167() V168() V169() V170() V171() V172() Element of bool NAT
x0 is epsilon-transitive epsilon-connected ordinal natural V30() V35() V42() real ext-real V59() V60() countable Element of dom G
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
yy0 . 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 left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,i0) is non empty set
[:NAT, the carrier of (G,i0):] is Relation-like V30() set
bool [:NAT, the carrier of (G,i0):] is V30() set
seqi is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,i0):]
lim seqi is Element of the carrier of (G,i0)
seqi is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,i0):]
lim seqi is Element of the carrier of (G,i0)
(G,x0) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V152() discerning reflexive RealNormSpace-like NORMSTR
the carrier of (G,x0) is non empty set
[:NAT, the carrier of (G,x0):] is Relation-like V30() set
bool [:NAT, the carrier of (G,x0):] is V30() set
seqi is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,x0):]
seqi is Relation-like Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of (G,x0):]
y0 is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
y0 . x0 is set
lim seqi is Element of the carrier of (G,x0)
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 . i is Element of the carrier of (G)
seqi . i is Element of the carrier of (G,x0)
x0 is Element of the carrier of (G)