REAL is non empty non trivial non finite V122() V123() V124() V128() set
NAT is non trivial ordinal non finite cardinal limit_cardinal V122() V123() V124() V125() V126() V127() V128() Element of bool REAL
bool REAL is non empty non trivial non finite set
omega is non trivial ordinal non finite cardinal limit_cardinal V122() V123() V124() V125() V126() V127() V128() set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite V122() V128() set
RAT is non empty non trivial non finite V122() V123() V124() V125() V128() set
INT is non empty non trivial non finite V122() V123() V124() V125() V126() V128() set
{} is set
the Function-like functional empty ext-real ordinal natural V36() real finite V42() cardinal {} -element FinSequence-membered V122() V123() V124() V125() V126() V127() V128() set is Function-like functional empty ext-real ordinal natural V36() real finite V42() cardinal {} -element FinSequence-membered V122() V123() V124() V125() V126() V127() V128() set
2 is non empty ext-real positive ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
1 is non empty ext-real positive ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
3 is non empty ext-real positive ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
Seg 1 is non empty trivial finite 1 -element V122() V123() V124() V125() V126() V127() Element of bool NAT
{1} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() set
Seg 2 is non empty finite 2 -element V122() V123() V124() V125() V126() V127() Element of bool NAT
{1,2} is finite V42() V122() V123() V124() V125() V126() V127() set
Seg 3 is non empty finite 3 -element V122() V123() V124() V125() V126() V127() Element of bool NAT
K89(1,2,3) is non empty finite V122() V123() V124() V125() V126() V127() set
0 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
- 1 is ext-real V36() real Element of REAL
dom {} is set
rng {} is set
R is 1-sorted
a is set
the carrier of R is set
R is non empty 1-sorted
the carrier of R is non empty set
a is Element of the carrier of R
(R,a) is Element of the carrier of R
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() addLoopStr
the carrier of R is non empty set
a is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
V is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len V is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
a + 1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
v is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len v is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
u is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len u is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom V is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
Seg a is finite a -element V122() V123() V124() V125() V126() V127() Element of bool NAT
V | (Seg a) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of R:]
[:NAT, the carrier of R:] is non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
v | (Seg a) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of R:]
u | (Seg a) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of R:]
k is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len k is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
Seg (a + 1) is finite a + 1 -element V122() V123() V124() V125() V126() V127() Element of bool NAT
dom v is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
v . (a + 1) is set
rng v is finite Element of bool the carrier of R
bool the carrier of R is non empty set
dom u is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
u . (a + 1) is set
rng u is finite Element of bool the carrier of R
V . (a + 1) is set
rng V is finite Element of bool the carrier of R
v1 is Element of the carrier of R
V /. (a + 1) is Element of the carrier of R
v /. (a + 1) is Element of the carrier of R
(V /. (a + 1)) + (v /. (a + 1)) is Element of the carrier of R
the addF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
the addF of R . ((V /. (a + 1)),(v /. (a + 1))) is Element of the carrier of R
[(V /. (a + 1)),(v /. (a + 1))] is set
{(V /. (a + 1)),(v /. (a + 1))} is finite set
{(V /. (a + 1))} is non empty trivial finite 1 -element set
{{(V /. (a + 1)),(v /. (a + 1))},{(V /. (a + 1))}} is finite V42() set
the addF of R . [(V /. (a + 1)),(v /. (a + 1))] is set
y is Element of the carrier of R
y + (v /. (a + 1)) is Element of the carrier of R
the addF of R . (y,(v /. (a + 1))) is Element of the carrier of R
[y,(v /. (a + 1))] is set
{y,(v /. (a + 1))} is finite set
{y} is non empty trivial finite 1 -element set
{{y,(v /. (a + 1))},{y}} is finite V42() set
the addF of R . [y,(v /. (a + 1))] is set
v is Element of the carrier of R
y + v is Element of the carrier of R
the addF of R . (y,v) is Element of the carrier of R
[y,v] is set
{y,v} is finite set
{{y,v},{y}} is finite V42() set
the addF of R . [y,v] is set
I is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
<*v*> is Relation-like NAT -defined the carrier of R -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like M13( the carrier of R,K353( the carrier of R))
K353( the carrier of R) is functional non empty FinSequence-membered M12( the carrier of R)
I ^ <*v*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum v is Element of the carrier of R
Sum I is Element of the carrier of R
Sum <*v*> is Element of the carrier of R
(Sum I) + (Sum <*v*>) is Element of the carrier of R
the addF of R . ((Sum I),(Sum <*v*>)) is Element of the carrier of R
[(Sum I),(Sum <*v*>)] is set
{(Sum I),(Sum <*v*>)} is finite set
{(Sum I)} is non empty trivial finite 1 -element set
{{(Sum I),(Sum <*v*>)},{(Sum I)}} is finite V42() set
the addF of R . [(Sum I),(Sum <*v*>)] is set
<*y*> is Relation-like NAT -defined the carrier of R -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like M13( the carrier of R,K353( the carrier of R))
Sum <*y*> is Element of the carrier of R
w is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len w is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
len I is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
v2 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom w is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
V . v2 is set
w . v2 is set
v /. v2 is Element of the carrier of R
v . v2 is set
dom k is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
u . v2 is set
k . v2 is set
V /. v2 is Element of the carrier of R
w /. v2 is Element of the carrier of R
dom I is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
I . v2 is set
I /. v2 is Element of the carrier of R
(w /. v2) + (I /. v2) is Element of the carrier of R
the addF of R . ((w /. v2),(I /. v2)) is Element of the carrier of R
[(w /. v2),(I /. v2)] is set
{(w /. v2),(I /. v2)} is finite set
{(w /. v2)} is non empty trivial finite 1 -element set
{{(w /. v2),(I /. v2)},{(w /. v2)}} is finite V42() set
the addF of R . [(w /. v2),(I /. v2)] is set
Sum k is Element of the carrier of R
Sum w is Element of the carrier of R
(Sum w) + (Sum I) is Element of the carrier of R
the addF of R . ((Sum w),(Sum I)) is Element of the carrier of R
[(Sum w),(Sum I)] is set
{(Sum w),(Sum I)} is finite set
{(Sum w)} is non empty trivial finite 1 -element set
{{(Sum w),(Sum I)},{(Sum w)}} is finite V42() set
the addF of R . [(Sum w),(Sum I)] is set
w ^ <*y*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum V is Element of the carrier of R
(Sum w) + (Sum <*y*>) is Element of the carrier of R
the addF of R . ((Sum w),(Sum <*y*>)) is Element of the carrier of R
[(Sum w),(Sum <*y*>)] is set
{(Sum w),(Sum <*y*>)} is finite set
{{(Sum w),(Sum <*y*>)},{(Sum w)}} is finite V42() set
the addF of R . [(Sum w),(Sum <*y*>)] is set
<*v1*> is Relation-like NAT -defined the carrier of R -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like M13( the carrier of R,K353( the carrier of R))
k ^ <*v1*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum u is Element of the carrier of R
Sum <*v1*> is Element of the carrier of R
(Sum k) + (Sum <*v1*>) is Element of the carrier of R
the addF of R . ((Sum k),(Sum <*v1*>)) is Element of the carrier of R
[(Sum k),(Sum <*v1*>)] is set
{(Sum k),(Sum <*v1*>)} is finite set
{(Sum k)} is non empty trivial finite 1 -element set
{{(Sum k),(Sum <*v1*>)},{(Sum k)}} is finite V42() set
the addF of R . [(Sum k),(Sum <*v1*>)] is set
((Sum w) + (Sum I)) + (y + v) is Element of the carrier of R
the addF of R . (((Sum w) + (Sum I)),(y + v)) is Element of the carrier of R
[((Sum w) + (Sum I)),(y + v)] is set
{((Sum w) + (Sum I)),(y + v)} is finite set
{((Sum w) + (Sum I))} is non empty trivial finite 1 -element set
{{((Sum w) + (Sum I)),(y + v)},{((Sum w) + (Sum I))}} is finite V42() set
the addF of R . [((Sum w) + (Sum I)),(y + v)] is set
((Sum w) + (Sum I)) + y is Element of the carrier of R
the addF of R . (((Sum w) + (Sum I)),y) is Element of the carrier of R
[((Sum w) + (Sum I)),y] is set
{((Sum w) + (Sum I)),y} is finite set
{{((Sum w) + (Sum I)),y},{((Sum w) + (Sum I))}} is finite V42() set
the addF of R . [((Sum w) + (Sum I)),y] is set
(((Sum w) + (Sum I)) + y) + v is Element of the carrier of R
the addF of R . ((((Sum w) + (Sum I)) + y),v) is Element of the carrier of R
[(((Sum w) + (Sum I)) + y),v] is set
{(((Sum w) + (Sum I)) + y),v} is finite set
{(((Sum w) + (Sum I)) + y)} is non empty trivial finite 1 -element set
{{(((Sum w) + (Sum I)) + y),v},{(((Sum w) + (Sum I)) + y)}} is finite V42() set
the addF of R . [(((Sum w) + (Sum I)) + y),v] is set
(Sum V) + (Sum I) is Element of the carrier of R
the addF of R . ((Sum V),(Sum I)) is Element of the carrier of R
[(Sum V),(Sum I)] is set
{(Sum V),(Sum I)} is finite set
{(Sum V)} is non empty trivial finite 1 -element set
{{(Sum V),(Sum I)},{(Sum V)}} is finite V42() set
the addF of R . [(Sum V),(Sum I)] is set
((Sum V) + (Sum I)) + v is Element of the carrier of R
the addF of R . (((Sum V) + (Sum I)),v) is Element of the carrier of R
[((Sum V) + (Sum I)),v] is set
{((Sum V) + (Sum I)),v} is finite set
{((Sum V) + (Sum I))} is non empty trivial finite 1 -element set
{{((Sum V) + (Sum I)),v},{((Sum V) + (Sum I))}} is finite V42() set
the addF of R . [((Sum V) + (Sum I)),v] is set
(Sum V) + (Sum v) is Element of the carrier of R
the addF of R . ((Sum V),(Sum v)) is Element of the carrier of R
[(Sum V),(Sum v)] is set
{(Sum V),(Sum v)} is finite set
{{(Sum V),(Sum v)},{(Sum V)}} is finite V42() set
the addF of R . [(Sum V),(Sum v)] is set
a is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
V is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len V is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
a + 1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
v is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len v is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
u is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len u is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom V is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
Sum u is Element of the carrier of R
Sum V is Element of the carrier of R
Sum v is Element of the carrier of R
(Sum V) + (Sum v) is Element of the carrier of R
the addF of R . ((Sum V),(Sum v)) is Element of the carrier of R
[(Sum V),(Sum v)] is set
{(Sum V),(Sum v)} is finite set
{(Sum V)} is non empty trivial finite 1 -element set
{{(Sum V),(Sum v)},{(Sum V)}} is finite V42() set
the addF of R . [(Sum V),(Sum v)] is set
a is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len a is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
V is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len V is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
v is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len v is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom a is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
Sum v is Element of the carrier of R
Sum a is Element of the carrier of R
Sum V is Element of the carrier of R
(Sum a) + (Sum V) is Element of the carrier of R
the addF of R . ((Sum a),(Sum V)) is Element of the carrier of R
[(Sum a),(Sum V)] is set
{(Sum a),(Sum V)} is finite set
{(Sum a)} is non empty trivial finite 1 -element set
{{(Sum a),(Sum V)},{(Sum a)}} is finite V42() set
the addF of R . [(Sum a),(Sum V)] is set
0. R is V57(R) Element of the carrier of R
the ZeroF of R is Element of the carrier of R
a is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len a is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
V is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len V is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
v is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len v is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom a is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
Sum v is Element of the carrier of R
Sum a is Element of the carrier of R
Sum V is Element of the carrier of R
(Sum a) + (Sum V) is Element of the carrier of R
the addF of R . ((Sum a),(Sum V)) is Element of the carrier of R
[(Sum a),(Sum V)] is set
{(Sum a),(Sum V)} is finite set
{(Sum a)} is non empty trivial finite 1 -element set
{{(Sum a),(Sum V)},{(Sum a)}} is finite V42() set
the addF of R . [(Sum a),(Sum V)] is set
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
the carrier of R is non empty set
a is ext-real V36() real Element of REAL
V is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len V is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom V is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
Sum V is Element of the carrier of R
a * (Sum V) is Element of the carrier of R
the Mult of R is Relation-like [:REAL, the carrier of R:] -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of R:], the carrier of R:]
[:REAL, the carrier of R:] is non empty non trivial non finite set
[:[:REAL, the carrier of R:], the carrier of R:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of R:], the carrier of R:] is non empty non trivial non finite set
the Mult of R . (a,(Sum V)) is set
[a,(Sum V)] is set
{a,(Sum V)} is finite set
{a} is non empty trivial finite 1 -element V122() V123() V124() set
{{a,(Sum V)},{a}} is finite V42() set
the Mult of R . [a,(Sum V)] is set
v is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len v is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
Sum v is Element of the carrier of R
Seg (len V) is finite len V -element V122() V123() V124() V125() V126() V127() Element of bool NAT
dom v is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
Seg (len v) is finite len v -element V122() V123() V124() V125() V126() V127() Element of bool NAT
u is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w is Element of the carrier of R
V . u is set
V /. u is Element of the carrier of R
v . u is set
a * w is Element of the carrier of R
the Mult of R . (a,w) is set
[a,w] is set
{a,w} is finite set
{{a,w},{a}} is finite V42() set
the Mult of R . [a,w] is set
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() addLoopStr
the carrier of R is non empty set
a is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len a is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
V is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len V is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom a is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
Sum V is Element of the carrier of R
Sum a is Element of the carrier of R
- (Sum a) is Element of the carrier of R
v is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom V is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
u is Element of the carrier of R
a . v is set
Seg (len V) is finite len V -element V122() V123() V124() V125() V126() V127() Element of bool NAT
Seg (len a) is finite len a -element V122() V123() V124() V125() V126() V127() Element of bool NAT
a /. v is Element of the carrier of R
V . v is set
- u is Element of the carrier of R
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() addLoopStr
the carrier of R is non empty set
a is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len a is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
V is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len V is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
v is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len v is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom a is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
Sum v is Element of the carrier of R
Sum a is Element of the carrier of R
Sum V is Element of the carrier of R
(Sum a) - (Sum V) is Element of the carrier of R
- (Sum V) is Element of the carrier of R
(Sum a) + (- (Sum V)) is Element of the carrier of R
the addF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
the addF of R . ((Sum a),(- (Sum V))) is Element of the carrier of R
[(Sum a),(- (Sum V))] is set
{(Sum a),(- (Sum V))} is finite set
{(Sum a)} is non empty trivial finite 1 -element set
{{(Sum a),(- (Sum V))},{(Sum a)}} is finite V42() set
the addF of R . [(Sum a),(- (Sum V))] is set
u is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len u is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom u is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
Seg (len V) is finite len V -element V122() V123() V124() V125() V126() V127() Element of bool NAT
dom V is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
w is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
u . w is set
V /. w is Element of the carrier of R
- (V /. w) is Element of the carrier of R
rng u is finite set
w is set
I is set
u . I is set
k is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
V /. k is Element of the carrier of R
- (V /. k) is Element of the carrier of R
y is Element of the carrier of R
I is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
Seg (len a) is finite len a -element V122() V123() V124() V125() V126() V127() Element of bool NAT
w is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom w is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
len w is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
Seg (len w) is finite len w -element V122() V123() V124() V125() V126() V127() Element of bool NAT
w . I is set
w /. I is Element of the carrier of R
v . I is set
a /. I is Element of the carrier of R
V /. I is Element of the carrier of R
(a /. I) - (V /. I) is Element of the carrier of R
- (V /. I) is Element of the carrier of R
(a /. I) + (- (V /. I)) is Element of the carrier of R
the addF of R . ((a /. I),(- (V /. I))) is Element of the carrier of R
[(a /. I),(- (V /. I))] is set
{(a /. I),(- (V /. I))} is finite set
{(a /. I)} is non empty trivial finite 1 -element set
{{(a /. I),(- (V /. I))},{(a /. I)}} is finite V42() set
the addF of R . [(a /. I),(- (V /. I))] is set
(a /. I) + (w /. I) is Element of the carrier of R
the addF of R . ((a /. I),(w /. I)) is Element of the carrier of R
[(a /. I),(w /. I)] is set
{(a /. I),(w /. I)} is finite set
{{(a /. I),(w /. I)},{(a /. I)}} is finite V42() set
the addF of R . [(a /. I),(w /. I)] is set
Sum w is Element of the carrier of R
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() addLoopStr
the carrier of R is non empty set
a is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom a is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
[:(dom a),(dom a):] is RAT -valued INT -valued finite V112() V113() V114() V115() set
bool [:(dom a),(dom a):] is non empty finite V42() set
len a is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
V is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len V is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom V is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
Sum a is Element of the carrier of R
Sum V is Element of the carrier of R
v is Relation-like dom a -defined dom a -valued Function-like one-to-one total quasi_total onto bijective finite V112() V113() V114() V115() Element of bool [:(dom a),(dom a):]
u is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len w is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
u + 1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
I is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len I is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
Seg u is finite u -element V122() V123() V124() V125() V126() V127() Element of bool NAT
I | (Seg u) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of R:]
[:NAT, the carrier of R:] is non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
dom w is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
[:(dom w),(dom w):] is RAT -valued INT -valued finite V112() V113() V114() V115() set
bool [:(dom w),(dom w):] is non empty finite V42() set
Seg (u + 1) is finite u + 1 -element V122() V123() V124() V125() V126() V127() Element of bool NAT
y is Relation-like dom w -defined dom w -valued Function-like one-to-one total quasi_total onto bijective finite V112() V113() V114() V115() Element of bool [:(dom w),(dom w):]
rng y is finite V122() V123() V124() V125() V126() V127() Element of bool (dom w)
bool (dom w) is non empty finite V42() set
v is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom y is finite V122() V123() V124() V125() V126() V127() Element of bool (dom w)
y . v is ext-real ordinal natural V36() real finite cardinal set
dom I is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
I . (u + 1) is set
k is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom k is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
len k is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
Seg (len k) is finite len k -element V122() V123() V124() V125() V126() V127() Element of bool NAT
y . (u + 1) is ext-real ordinal natural V36() real finite cardinal set
v1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
v2 is ext-real ordinal natural V36() real finite cardinal set
v1 + v2 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
n is ext-real ordinal natural V36() real finite cardinal set
1 + n is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
u is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
Seg u is finite u -element V122() V123() V124() V125() V126() V127() Element of bool NAT
q2 is ext-real ordinal natural V36() real finite cardinal set
v1 + q2 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w . (v1 + q2) is set
q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom q2 is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
rng q2 is finite set
q2 is set
q1 is set
q2 . q1 is set
g is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
v1 + g is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w . (v1 + g) is set
q is Element of the carrier of R
w is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
Seg w is finite w -element V122() V123() V124() V125() V126() V127() Element of bool NAT
w | (Seg w) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of R:]
q1 is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom q1 is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
g is ext-real ordinal natural V36() real finite cardinal set
y . g is ext-real ordinal natural V36() real finite cardinal set
q is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
q - 1 is ext-real V36() real Element of REAL
g is ext-real V36() real Element of REAL
g is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
g - 1 is ext-real V36() real Element of REAL
q is ext-real V36() real Element of REAL
g is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom g is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
g is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
q is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
y . q is ext-real ordinal natural V36() real finite cardinal set
w + 1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
u + 0 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
(w + 1) + 1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w + 2 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
len q1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
q is ext-real ordinal natural V36() real finite cardinal set
q2 is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom q2 is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
v is Element of the carrier of R
<*v*> is Relation-like NAT -defined the carrier of R -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like M13( the carrier of R,K353( the carrier of R))
K353( the carrier of R) is functional non empty FinSequence-membered M12( the carrier of R)
q1 ^ <*v*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len (q1 ^ <*v*>) is non empty ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
len <*v*> is non empty ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w + (len <*v*>) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
(len (q1 ^ <*v*>)) + q is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w . ((len (q1 ^ <*v*>)) + q) is set
q2 . q is set
1 + u is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w + u is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
1 + (w + u) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
rng g is finite set
q is set
g is set
g . g is set
g is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
y . g is ext-real ordinal natural V36() real finite cardinal set
g . g is set
g is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
y . g is ext-real ordinal natural V36() real finite cardinal set
i is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
i - 1 is ext-real V36() real Element of REAL
j is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
(u + 1) - 1 is ext-real V36() real Element of REAL
(w + 2) - 1 is ext-real V36() real Element of REAL
g . g is set
g is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
y . g is ext-real ordinal natural V36() real finite cardinal set
q1 ^ q2 is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len q2 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
len (q1 ^ q2) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom (q1 ^ q2) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
[:(dom (q1 ^ q2)),(dom (q1 ^ q2)):] is RAT -valued INT -valued finite V112() V113() V114() V115() set
bool [:(dom (q1 ^ q2)),(dom (q1 ^ q2)):] is non empty finite V42() set
g is Relation-like dom (q1 ^ q2) -defined dom (q1 ^ q2) -valued Function-like total quasi_total finite V112() V113() V114() V115() Element of bool [:(dom (q1 ^ q2)),(dom (q1 ^ q2)):]
rng g is finite V122() V123() V124() V125() V126() V127() Element of bool (dom (q1 ^ q2))
bool (dom (q1 ^ q2)) is non empty finite V42() set
g is set
j is set
y . j is ext-real ordinal natural V36() real finite cardinal set
j1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom g is finite V122() V123() V124() V125() V126() V127() Element of bool (dom (q1 ^ q2))
y . j1 is ext-real ordinal natural V36() real finite cardinal set
g . j1 is ext-real ordinal natural V36() real finite cardinal set
y . j1 is ext-real ordinal natural V36() real finite cardinal set
i is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
i + 1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
a is set
y . a is ext-real ordinal natural V36() real finite cardinal set
(Seg (u + 1)) \ (Seg u) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
{(u + 1)} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() Element of bool REAL
g . a is ext-real ordinal natural V36() real finite cardinal set
(i + 1) - 1 is ext-real V36() real Element of REAL
y . j1 is ext-real ordinal natural V36() real finite cardinal set
j1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom g is finite V122() V123() V124() V125() V126() V127() Element of bool (dom (q1 ^ q2))
i is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
i + 1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
a is set
y . a is ext-real ordinal natural V36() real finite cardinal set
(Seg (u + 1)) \ (Seg u) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
{(u + 1)} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() Element of bool REAL
i + 0 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
g . a is ext-real ordinal natural V36() real finite cardinal set
(i + 1) - 1 is ext-real V36() real Element of REAL
j1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom g is finite V122() V123() V124() V125() V126() V127() Element of bool (dom (q1 ^ q2))
w . (y . (u + 1)) is set
g is ext-real ordinal natural V36() real finite cardinal set
dom (q1 ^ <*v*>) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
q1 . g is set
w . g is set
(q1 ^ <*v*>) . g is set
dom <*v*> is non empty trivial finite 1 -element V122() V123() V124() V125() V126() V127() Element of bool NAT
(len q1) + 1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
(q1 ^ <*v*>) . ((len q1) + 1) is set
<*v*> . 1 is set
{v1} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() set
Seg (w + 1) is finite w + 1 -element V122() V123() V124() V125() V126() V127() Element of bool NAT
(Seg w) \/ {v1} is finite V122() V123() V124() V125() V126() V127() set
g is set
dom g is finite set
g . g is ext-real ordinal natural V36() real finite cardinal set
i is set
g . i is ext-real ordinal natural V36() real finite cardinal set
dom g is finite V122() V123() V124() V125() V126() V127() Element of bool (dom (q1 ^ q2))
y . i is ext-real ordinal natural V36() real finite cardinal set
y . g is ext-real ordinal natural V36() real finite cardinal set
j is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
g . j is ext-real ordinal natural V36() real finite cardinal set
j1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
g . j1 is ext-real ordinal natural V36() real finite cardinal set
a is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
j is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
g . j is ext-real ordinal natural V36() real finite cardinal set
j1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
g . j1 is ext-real ordinal natural V36() real finite cardinal set
b is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
b - 1 is ext-real V36() real Element of REAL
(b - 1) + 1 is ext-real V36() real Element of REAL
(Seg (w + 1)) \ (Seg w) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
{(w + 1)} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() Element of bool REAL
b is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
j is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
g . j is ext-real ordinal natural V36() real finite cardinal set
a is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
a - 1 is ext-real V36() real Element of REAL
j1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
g . j1 is ext-real ordinal natural V36() real finite cardinal set
(a - 1) + 1 is ext-real V36() real Element of REAL
(Seg (w + 1)) \ (Seg w) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
{(w + 1)} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() Element of bool REAL
j1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
g . j1 is ext-real ordinal natural V36() real finite cardinal set
b is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
b - 1 is ext-real V36() real Element of REAL
b + (- 1) is ext-real V36() real Element of REAL
j is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
g . j is ext-real ordinal natural V36() real finite cardinal set
a is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
a - 1 is ext-real V36() real Element of REAL
a + (- 1) is ext-real V36() real Element of REAL
(len (q1 ^ <*v*>)) + (len q2) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
(len q1) + (len <*v*>) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
((len q1) + (len <*v*>)) + u is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
Seg ((len (q1 ^ <*v*>)) + (len q2)) is finite (len (q1 ^ <*v*>)) + (len q2) -element V122() V123() V124() V125() V126() V127() Element of bool NAT
(q1 ^ <*v*>) ^ q2 is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
i is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
y . i is ext-real ordinal natural V36() real finite cardinal set
g is Relation-like dom (q1 ^ q2) -defined dom (q1 ^ q2) -valued Function-like one-to-one total quasi_total onto bijective finite V112() V113() V114() V115() Element of bool [:(dom (q1 ^ q2)),(dom (q1 ^ q2)):]
g . i is ext-real ordinal natural V36() real finite cardinal set
j is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w . j is set
q1 . j is set
I . i is set
k . i is set
w . (y . i) is set
(q1 ^ q2) . (g . i) is set
j is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
(w + 2) - 1 is ext-real V36() real Element of REAL
j - 1 is ext-real V36() real Element of REAL
j1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
g is Relation-like dom (q1 ^ q2) -defined dom (q1 ^ q2) -valued Function-like one-to-one total quasi_total onto bijective finite V112() V113() V114() V115() Element of bool [:(dom (q1 ^ q2)),(dom (q1 ^ q2)):]
g . i is ext-real ordinal natural V36() real finite cardinal set
a is ext-real ordinal natural V36() real finite cardinal set
(len q1) + a is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
I . i is set
k . i is set
w . (y . i) is set
<*v*> ^ q2 is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
q1 ^ (<*v*> ^ q2) is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom (<*v*> ^ q2) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
b is ext-real ordinal natural V36() real finite cardinal set
(len q1) + b is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w . j is set
(<*v*> ^ q2) . b is set
1 + a is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
(q1 ^ q2) . (j - 1) is set
q2 . a is set
(q1 ^ q2) . (g . i) is set
k . i is set
g is Relation-like dom (q1 ^ q2) -defined dom (q1 ^ q2) -valued Function-like one-to-one total quasi_total onto bijective finite V112() V113() V114() V115() Element of bool [:(dom (q1 ^ q2)),(dom (q1 ^ q2)):]
g . i is ext-real ordinal natural V36() real finite cardinal set
(q1 ^ q2) . (g . i) is set
k . i is set
g is Relation-like dom (q1 ^ q2) -defined dom (q1 ^ q2) -valued Function-like one-to-one total quasi_total onto bijective finite V112() V113() V114() V115() Element of bool [:(dom (q1 ^ q2)),(dom (q1 ^ q2)):]
g . i is ext-real ordinal natural V36() real finite cardinal set
(q1 ^ q2) . (g . i) is set
Sum k is Element of the carrier of R
Sum (q1 ^ q2) is Element of the carrier of R
Sum I is Element of the carrier of R
Sum <*v*> is Element of the carrier of R
(Sum (q1 ^ q2)) + (Sum <*v*>) is Element of the carrier of R
the addF of R is Relation-like [: the carrier of R, the carrier of R:] -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
the addF of R . ((Sum (q1 ^ q2)),(Sum <*v*>)) is Element of the carrier of R
[(Sum (q1 ^ q2)),(Sum <*v*>)] is set
{(Sum (q1 ^ q2)),(Sum <*v*>)} is finite set
{(Sum (q1 ^ q2))} is non empty trivial finite 1 -element set
{{(Sum (q1 ^ q2)),(Sum <*v*>)},{(Sum (q1 ^ q2))}} is finite V42() set
the addF of R . [(Sum (q1 ^ q2)),(Sum <*v*>)] is set
Sum q1 is Element of the carrier of R
Sum q2 is Element of the carrier of R
(Sum q1) + (Sum q2) is Element of the carrier of R
the addF of R . ((Sum q1),(Sum q2)) is Element of the carrier of R
[(Sum q1),(Sum q2)] is set
{(Sum q1),(Sum q2)} is finite set
{(Sum q1)} is non empty trivial finite 1 -element set
{{(Sum q1),(Sum q2)},{(Sum q1)}} is finite V42() set
the addF of R . [(Sum q1),(Sum q2)] is set
((Sum q1) + (Sum q2)) + (Sum <*v*>) is Element of the carrier of R
the addF of R . (((Sum q1) + (Sum q2)),(Sum <*v*>)) is Element of the carrier of R
[((Sum q1) + (Sum q2)),(Sum <*v*>)] is set
{((Sum q1) + (Sum q2)),(Sum <*v*>)} is finite set
{((Sum q1) + (Sum q2))} is non empty trivial finite 1 -element set
{{((Sum q1) + (Sum q2)),(Sum <*v*>)},{((Sum q1) + (Sum q2))}} is finite V42() set
the addF of R . [((Sum q1) + (Sum q2)),(Sum <*v*>)] is set
(Sum <*v*>) + (Sum q2) is Element of the carrier of R
the addF of R . ((Sum <*v*>),(Sum q2)) is Element of the carrier of R
[(Sum <*v*>),(Sum q2)] is set
{(Sum <*v*>),(Sum q2)} is finite set
{(Sum <*v*>)} is non empty trivial finite 1 -element set
{{(Sum <*v*>),(Sum q2)},{(Sum <*v*>)}} is finite V42() set
the addF of R . [(Sum <*v*>),(Sum q2)] is set
(Sum q1) + ((Sum <*v*>) + (Sum q2)) is Element of the carrier of R
the addF of R . ((Sum q1),((Sum <*v*>) + (Sum q2))) is Element of the carrier of R
[(Sum q1),((Sum <*v*>) + (Sum q2))] is set
{(Sum q1),((Sum <*v*>) + (Sum q2))} is finite set
{{(Sum q1),((Sum <*v*>) + (Sum q2))},{(Sum q1)}} is finite V42() set
the addF of R . [(Sum q1),((Sum <*v*>) + (Sum q2))] is set
<*v*> ^ q2 is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (<*v*> ^ q2) is Element of the carrier of R
(Sum q1) + (Sum (<*v*> ^ q2)) is Element of the carrier of R
the addF of R . ((Sum q1),(Sum (<*v*> ^ q2))) is Element of the carrier of R
[(Sum q1),(Sum (<*v*> ^ q2))] is set
{(Sum q1),(Sum (<*v*> ^ q2))} is finite set
{{(Sum q1),(Sum (<*v*> ^ q2))},{(Sum q1)}} is finite V42() set
the addF of R . [(Sum q1),(Sum (<*v*> ^ q2))] is set
q1 ^ (<*v*> ^ q2) is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (q1 ^ (<*v*> ^ q2)) is Element of the carrier of R
Sum w is Element of the carrier of R
w is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom w is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
[:(dom w),(dom w):] is RAT -valued INT -valued finite V112() V113() V114() V115() set
bool [:(dom w),(dom w):] is non empty finite V42() set
u is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
len w is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
u + 1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
I is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len I is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom I is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
k is Relation-like dom w -defined dom w -valued Function-like one-to-one total quasi_total onto bijective finite V112() V113() V114() V115() Element of bool [:(dom w),(dom w):]
Sum w is Element of the carrier of R
Sum I is Element of the carrier of R
u is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len u is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len w is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom u is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
[:(dom u),(dom u):] is RAT -valued INT -valued finite V112() V113() V114() V115() set
bool [:(dom u),(dom u):] is non empty finite V42() set
dom w is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
Sum u is Element of the carrier of R
Sum w is Element of the carrier of R
0. R is V57(R) Element of the carrier of R
the ZeroF of R is Element of the carrier of R
I is Relation-like dom u -defined dom u -valued Function-like one-to-one total quasi_total onto bijective finite V112() V113() V114() V115() Element of bool [:(dom u),(dom u):]
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() addLoopStr
the carrier of R is non empty set
a is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom a is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
[:(dom a),(dom a):] is RAT -valued INT -valued finite V112() V113() V114() V115() set
bool [:(dom a),(dom a):] is non empty finite V42() set
V is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum a is Element of the carrier of R
Sum V is Element of the carrier of R
v is Relation-like dom a -defined dom a -valued Function-like one-to-one total quasi_total onto bijective finite V112() V113() V114() V115() Element of bool [:(dom a),(dom a):]
a * v is Relation-like dom a -defined the carrier of R -valued Function-like finite Element of bool [:(dom a), the carrier of R:]
[:(dom a), the carrier of R:] is set
bool [:(dom a), the carrier of R:] is non empty set
len a is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
len V is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom V is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
u is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
V . u is set
v . u is ext-real ordinal natural V36() real finite cardinal set
a . (v . u) is set
R is non empty addLoopStr
the carrier of R is non empty set
bool the carrier of R is non empty set
a is finite Element of bool the carrier of R
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng V is finite set
v is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum v is Element of the carrier of R
rng v is finite Element of bool the carrier of R
u is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
rng u is finite Element of bool the carrier of R
V is Element of the carrier of R
Sum u is Element of the carrier of R
w is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
rng w is finite Element of bool the carrier of R
v is Element of the carrier of R
Sum w is Element of the carrier of R
R is non empty Abelian add-associative right_zeroed V108() addLoopStr
{} R is Function-like functional empty proper ext-real ordinal natural V36() real finite V42() cardinal {} -element FinSequence-membered V122() V123() V124() V125() V126() V127() V128() Element of bool the carrier of R
the carrier of R is non empty set
bool the carrier of R is non empty set
(R,({} R)) is Element of the carrier of R
0. R is V57(R) Element of the carrier of R
the ZeroF of R is Element of the carrier of R
<*> the carrier of R is Relation-like NAT -defined the carrier of R -valued Function-like one-to-one constant functional empty ext-real ordinal natural V36() real finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V112() V113() V114() V115() V122() V123() V124() V125() V126() V127() V128() M13( the carrier of R,K353( the carrier of R))
K353( the carrier of R) is functional non empty