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