:: RLVECT_2 semantic presentation

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 FinSequence-membered M12( the carrier of R)
Sum (<*> the carrier of R) 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 Element of the carrier of R
{a} is non empty trivial finite 1 -element Element of bool the carrier of R
bool the carrier of R is non empty set
(R,{a}) is Element of the carrier of R
<*a*> 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)
Sum <*a*> is Element of the carrier of R
rng <*a*> is trivial finite Element of bool 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 Element of the carrier of R
V is Element of the carrier of R
{a,V} is finite Element of bool the carrier of R
bool the carrier of R is non empty set
(R,{a,V}) is Element of the carrier of R
a + 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 . (a,V) is Element of the carrier of R
[a,V] is set
{a,V} is finite set
{a} is non empty trivial finite 1 -element set
{{a,V},{a}} is finite V42() set
the addF of R . [a,V] is set
<*a,V*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R
rng <*a,V*> is finite Element of bool the carrier of R
Sum <*a,V*> 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 Element of the carrier of R
V is Element of the carrier of R
v is Element of the carrier of R
{a,V,v} is non empty finite Element of bool the carrier of R
bool the carrier of R is non empty set
(R,{a,V,v}) is Element of the carrier of R
a + 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 . (a,V) is Element of the carrier of R
[a,V] is set
{a,V} is finite set
{a} is non empty trivial finite 1 -element set
{{a,V},{a}} is finite V42() set
the addF of R . [a,V] is set
(a + V) + v is Element of the carrier of R
the addF of R . ((a + V),v) is Element of the carrier of R
[(a + V),v] is set
{(a + V),v} is finite set
{(a + V)} is non empty trivial finite 1 -element set
{{(a + V),v},{(a + V)}} is finite V42() set
the addF of R . [(a + V),v] is set
<*a,V,v*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R
rng <*a,V,v*> is finite Element of bool the carrier of R
Sum <*a,V,v*> is Element of the carrier of R
R is non empty Abelian add-associative right_zeroed V108() addLoopStr
the carrier of R is non empty set
bool the carrier of R is non empty set
V is finite Element of bool the carrier of R
a is finite Element of bool the carrier of R
V \/ a is finite Element of bool the carrier of R
(R,(V \/ a)) is Element of the carrier of R
(R,V) is Element of the carrier of R
(R,a) is Element of the carrier of R
(R,V) + (R,a) 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 . ((R,V),(R,a)) is Element of the carrier of R
[(R,V),(R,a)] is set
{(R,V),(R,a)} is finite set
{(R,V)} is non empty trivial finite 1 -element set
{{(R,V),(R,a)},{(R,V)}} is finite V42() set
the addF of R . [(R,V),(R,a)] 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
rng v is finite Element of bool the carrier of R
Sum v 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
rng u is finite Element of bool 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
Sum w is Element of the carrier of R
u ^ 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 (u ^ w) is finite Element of bool the carrier of R
Sum (u ^ 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
bool the carrier of R is non empty set
V is finite Element of bool the carrier of R
a is finite Element of bool the carrier of R
V \/ a is finite Element of bool the carrier of R
(R,(V \/ a)) is Element of the carrier of R
(R,V) is Element of the carrier of R
(R,a) is Element of the carrier of R
(R,V) + (R,a) 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 . ((R,V),(R,a)) is Element of the carrier of R
[(R,V),(R,a)] is set
{(R,V),(R,a)} is finite set
{(R,V)} is non empty trivial finite 1 -element set
{{(R,V),(R,a)},{(R,V)}} is finite V42() set
the addF of R . [(R,V),(R,a)] is set
V /\ a is finite Element of bool the carrier of R
(R,(V /\ a)) is Element of the carrier of R
((R,V) + (R,a)) - (R,(V /\ a)) is Element of the carrier of R
- (R,(V /\ a)) is Element of the carrier of R
((R,V) + (R,a)) + (- (R,(V /\ a))) is Element of the carrier of R
the addF of R . (((R,V) + (R,a)),(- (R,(V /\ a)))) is Element of the carrier of R
[((R,V) + (R,a)),(- (R,(V /\ a)))] is set
{((R,V) + (R,a)),(- (R,(V /\ a)))} is finite set
{((R,V) + (R,a))} is non empty trivial finite 1 -element set
{{((R,V) + (R,a)),(- (R,(V /\ a)))},{((R,V) + (R,a))}} is finite V42() set
the addF of R . [((R,V) + (R,a)),(- (R,(V /\ a)))] is set
a \ V is finite Element of bool the carrier of R
V \ a is finite Element of bool the carrier of R
(a \ V) \/ (V \ a) is finite Element of bool the carrier of R
(a \ V) \/ (V /\ a) is finite Element of bool the carrier of R
(V \ a) \/ (V /\ a) is finite Element of bool the carrier of R
V \+\ a is finite Element of bool the carrier of R
V \ a is finite set
a \ V is finite set
(V \ a) \/ (a \ V) is finite set
((a \ V) \/ (V \ a)) \/ (V /\ a) is finite Element of bool the carrier of R
(R,(V \/ a)) + (R,(V /\ a)) is Element of the carrier of R
the addF of R . ((R,(V \/ a)),(R,(V /\ a))) is Element of the carrier of R
[(R,(V \/ a)),(R,(V /\ a))] is set
{(R,(V \/ a)),(R,(V /\ a))} is finite set
{(R,(V \/ a))} is non empty trivial finite 1 -element set
{{(R,(V \/ a)),(R,(V /\ a))},{(R,(V \/ a))}} is finite V42() set
the addF of R . [(R,(V \/ a)),(R,(V /\ a))] is set
(R,((a \ V) \/ (V \ a))) is Element of the carrier of R
(R,((a \ V) \/ (V \ a))) + (R,(V /\ a)) is Element of the carrier of R
the addF of R . ((R,((a \ V) \/ (V \ a))),(R,(V /\ a))) is Element of the carrier of R
[(R,((a \ V) \/ (V \ a))),(R,(V /\ a))] is set
{(R,((a \ V) \/ (V \ a))),(R,(V /\ a))} is finite set
{(R,((a \ V) \/ (V \ a)))} is non empty trivial finite 1 -element set
{{(R,((a \ V) \/ (V \ a))),(R,(V /\ a))},{(R,((a \ V) \/ (V \ a)))}} is finite V42() set
the addF of R . [(R,((a \ V) \/ (V \ a))),(R,(V /\ a))] is set
((R,((a \ V) \/ (V \ a))) + (R,(V /\ a))) + (R,(V /\ a)) is Element of the carrier of R
the addF of R . (((R,((a \ V) \/ (V \ a))) + (R,(V /\ a))),(R,(V /\ a))) is Element of the carrier of R
[((R,((a \ V) \/ (V \ a))) + (R,(V /\ a))),(R,(V /\ a))] is set
{((R,((a \ V) \/ (V \ a))) + (R,(V /\ a))),(R,(V /\ a))} is finite set
{((R,((a \ V) \/ (V \ a))) + (R,(V /\ a)))} is non empty trivial finite 1 -element set
{{((R,((a \ V) \/ (V \ a))) + (R,(V /\ a))),(R,(V /\ a))},{((R,((a \ V) \/ (V \ a))) + (R,(V /\ a)))}} is finite V42() set
the addF of R . [((R,((a \ V) \/ (V \ a))) + (R,(V /\ a))),(R,(V /\ a))] is set
(R,(a \ V)) is Element of the carrier of R
(R,(V \ a)) is Element of the carrier of R
(R,(a \ V)) + (R,(V \ a)) is Element of the carrier of R
the addF of R . ((R,(a \ V)),(R,(V \ a))) is Element of the carrier of R
[(R,(a \ V)),(R,(V \ a))] is set
{(R,(a \ V)),(R,(V \ a))} is finite set
{(R,(a \ V))} is non empty trivial finite 1 -element set
{{(R,(a \ V)),(R,(V \ a))},{(R,(a \ V))}} is finite V42() set
the addF of R . [(R,(a \ V)),(R,(V \ a))] is set
((R,(a \ V)) + (R,(V \ a))) + (R,(V /\ a)) is Element of the carrier of R
the addF of R . (((R,(a \ V)) + (R,(V \ a))),(R,(V /\ a))) is Element of the carrier of R
[((R,(a \ V)) + (R,(V \ a))),(R,(V /\ a))] is set
{((R,(a \ V)) + (R,(V \ a))),(R,(V /\ a))} is finite set
{((R,(a \ V)) + (R,(V \ a)))} is non empty trivial finite 1 -element set
{{((R,(a \ V)) + (R,(V \ a))),(R,(V /\ a))},{((R,(a \ V)) + (R,(V \ a)))}} is finite V42() set
the addF of R . [((R,(a \ V)) + (R,(V \ a))),(R,(V /\ a))] is set
(((R,(a \ V)) + (R,(V \ a))) + (R,(V /\ a))) + (R,(V /\ a)) is Element of the carrier of R
the addF of R . ((((R,(a \ V)) + (R,(V \ a))) + (R,(V /\ a))),(R,(V /\ a))) is Element of the carrier of R
[(((R,(a \ V)) + (R,(V \ a))) + (R,(V /\ a))),(R,(V /\ a))] is set
{(((R,(a \ V)) + (R,(V \ a))) + (R,(V /\ a))),(R,(V /\ a))} is finite set
{(((R,(a \ V)) + (R,(V \ a))) + (R,(V /\ a)))} is non empty trivial finite 1 -element set
{{(((R,(a \ V)) + (R,(V \ a))) + (R,(V /\ a))),(R,(V /\ a))},{(((R,(a \ V)) + (R,(V \ a))) + (R,(V /\ a)))}} is finite V42() set
the addF of R . [(((R,(a \ V)) + (R,(V \ a))) + (R,(V /\ a))),(R,(V /\ a))] is set
(R,(V /\ a)) + (R,(V \ a)) is Element of the carrier of R
the addF of R . ((R,(V /\ a)),(R,(V \ a))) is Element of the carrier of R
[(R,(V /\ a)),(R,(V \ a))] is set
{(R,(V /\ a)),(R,(V \ a))} is finite set
{(R,(V /\ a))} is non empty trivial finite 1 -element set
{{(R,(V /\ a)),(R,(V \ a))},{(R,(V /\ a))}} is finite V42() set
the addF of R . [(R,(V /\ a)),(R,(V \ a))] is set
(R,(a \ V)) + ((R,(V /\ a)) + (R,(V \ a))) is Element of the carrier of R
the addF of R . ((R,(a \ V)),((R,(V /\ a)) + (R,(V \ a)))) is Element of the carrier of R
[(R,(a \ V)),((R,(V /\ a)) + (R,(V \ a)))] is set
{(R,(a \ V)),((R,(V /\ a)) + (R,(V \ a)))} is finite set
{{(R,(a \ V)),((R,(V /\ a)) + (R,(V \ a)))},{(R,(a \ V))}} is finite V42() set
the addF of R . [(R,(a \ V)),((R,(V /\ a)) + (R,(V \ a)))] is set
((R,(a \ V)) + ((R,(V /\ a)) + (R,(V \ a)))) + (R,(V /\ a)) is Element of the carrier of R
the addF of R . (((R,(a \ V)) + ((R,(V /\ a)) + (R,(V \ a)))),(R,(V /\ a))) is Element of the carrier of R
[((R,(a \ V)) + ((R,(V /\ a)) + (R,(V \ a)))),(R,(V /\ a))] is set
{((R,(a \ V)) + ((R,(V /\ a)) + (R,(V \ a)))),(R,(V /\ a))} is finite set
{((R,(a \ V)) + ((R,(V /\ a)) + (R,(V \ a))))} is non empty trivial finite 1 -element set
{{((R,(a \ V)) + ((R,(V /\ a)) + (R,(V \ a)))),(R,(V /\ a))},{((R,(a \ V)) + ((R,(V /\ a)) + (R,(V \ a))))}} is finite V42() set
the addF of R . [((R,(a \ V)) + ((R,(V /\ a)) + (R,(V \ a)))),(R,(V /\ a))] is set
(R,(a \ V)) + (R,(V /\ a)) is Element of the carrier of R
the addF of R . ((R,(a \ V)),(R,(V /\ a))) is Element of the carrier of R
[(R,(a \ V)),(R,(V /\ a))] is set
{(R,(a \ V)),(R,(V /\ a))} is finite set
{{(R,(a \ V)),(R,(V /\ a))},{(R,(a \ V))}} is finite V42() set
the addF of R . [(R,(a \ V)),(R,(V /\ a))] is set
(R,(V \ a)) + (R,(V /\ a)) is Element of the carrier of R
the addF of R . ((R,(V \ a)),(R,(V /\ a))) is Element of the carrier of R
[(R,(V \ a)),(R,(V /\ a))] is set
{(R,(V \ a)),(R,(V /\ a))} is finite set
{(R,(V \ a))} is non empty trivial finite 1 -element set
{{(R,(V \ a)),(R,(V /\ a))},{(R,(V \ a))}} is finite V42() set
the addF of R . [(R,(V \ a)),(R,(V /\ a))] is set
((R,(a \ V)) + (R,(V /\ a))) + ((R,(V \ a)) + (R,(V /\ a))) is Element of the carrier of R
the addF of R . (((R,(a \ V)) + (R,(V /\ a))),((R,(V \ a)) + (R,(V /\ a)))) is Element of the carrier of R
[((R,(a \ V)) + (R,(V /\ a))),((R,(V \ a)) + (R,(V /\ a)))] is set
{((R,(a \ V)) + (R,(V /\ a))),((R,(V \ a)) + (R,(V /\ a)))} is finite set
{((R,(a \ V)) + (R,(V /\ a)))} is non empty trivial finite 1 -element set
{{((R,(a \ V)) + (R,(V /\ a))),((R,(V \ a)) + (R,(V /\ a)))},{((R,(a \ V)) + (R,(V /\ a)))}} is finite V42() set
the addF of R . [((R,(a \ V)) + (R,(V /\ a))),((R,(V \ a)) + (R,(V /\ a)))] is set
(R,a) + ((R,(V \ a)) + (R,(V /\ a))) is Element of the carrier of R
the addF of R . ((R,a),((R,(V \ a)) + (R,(V /\ a)))) is Element of the carrier of R
[(R,a),((R,(V \ a)) + (R,(V /\ a)))] is set
{(R,a),((R,(V \ a)) + (R,(V /\ a)))} is finite set
{(R,a)} is non empty trivial finite 1 -element set
{{(R,a),((R,(V \ a)) + (R,(V /\ a)))},{(R,a)}} is finite V42() set
the addF of R . [(R,a),((R,(V \ a)) + (R,(V /\ a)))] 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
bool the carrier of R is non empty set
V is finite Element of bool the carrier of R
a is finite Element of bool the carrier of R
V /\ a is finite Element of bool the carrier of R
(R,(V /\ a)) is Element of the carrier of R
(R,V) is Element of the carrier of R
(R,a) is Element of the carrier of R
(R,V) + (R,a) 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 . ((R,V),(R,a)) is Element of the carrier of R
[(R,V),(R,a)] is set
{(R,V),(R,a)} is finite set
{(R,V)} is non empty trivial finite 1 -element set
{{(R,V),(R,a)},{(R,V)}} is finite V42() set
the addF of R . [(R,V),(R,a)] is set
V \/ a is finite Element of bool the carrier of R
(R,(V \/ a)) is Element of the carrier of R
((R,V) + (R,a)) - (R,(V \/ a)) is Element of the carrier of R
- (R,(V \/ a)) is Element of the carrier of R
((R,V) + (R,a)) + (- (R,(V \/ a))) is Element of the carrier of R
the addF of R . (((R,V) + (R,a)),(- (R,(V \/ a)))) is Element of the carrier of R
[((R,V) + (R,a)),(- (R,(V \/ a)))] is set
{((R,V) + (R,a)),(- (R,(V \/ a)))} is finite set
{((R,V) + (R,a))} is non empty trivial finite 1 -element set
{{((R,V) + (R,a)),(- (R,(V \/ a)))},{((R,V) + (R,a))}} is finite V42() set
the addF of R . [((R,V) + (R,a)),(- (R,(V \/ a)))] is set
((R,V) + (R,a)) - (R,(V /\ a)) is Element of the carrier of R
- (R,(V /\ a)) is Element of the carrier of R
((R,V) + (R,a)) + (- (R,(V /\ a))) is Element of the carrier of R
the addF of R . (((R,V) + (R,a)),(- (R,(V /\ a)))) is Element of the carrier of R
[((R,V) + (R,a)),(- (R,(V /\ a)))] is set
{((R,V) + (R,a)),(- (R,(V /\ a)))} is finite set
{{((R,V) + (R,a)),(- (R,(V /\ a)))},{((R,V) + (R,a))}} is finite V42() set
the addF of R . [((R,V) + (R,a)),(- (R,(V /\ a)))] is set
(R,(V /\ a)) + (R,(V \/ a)) is Element of the carrier of R
the addF of R . ((R,(V /\ a)),(R,(V \/ a))) is Element of the carrier of R
[(R,(V /\ a)),(R,(V \/ a))] is set
{(R,(V /\ a)),(R,(V \/ a))} is finite set
{(R,(V /\ a))} is non empty trivial finite 1 -element set
{{(R,(V /\ a)),(R,(V \/ a))},{(R,(V /\ a))}} is finite V42() set
the addF of R . [(R,(V /\ a)),(R,(V \/ a))] 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
bool the carrier of R is non empty set
V is finite Element of bool the carrier of R
a is finite Element of bool the carrier of R
V \ a is finite Element of bool the carrier of R
(R,(V \ a)) is Element of the carrier of R
V \/ a is finite Element of bool the carrier of R
(R,(V \/ a)) is Element of the carrier of R
(R,a) is Element of the carrier of R
(R,(V \/ a)) - (R,a) is Element of the carrier of R
- (R,a) is Element of the carrier of R
(R,(V \/ a)) + (- (R,a)) 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 . ((R,(V \/ a)),(- (R,a))) is Element of the carrier of R
[(R,(V \/ a)),(- (R,a))] is set
{(R,(V \/ a)),(- (R,a))} is finite set
{(R,(V \/ a))} is non empty trivial finite 1 -element set
{{(R,(V \/ a)),(- (R,a))},{(R,(V \/ a))}} is finite V42() set
the addF of R . [(R,(V \/ a)),(- (R,a))] is set
(V \ a) /\ a is finite Element of bool the carrier of R
{} 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
(V \ a) \/ a is finite Element of bool the carrier of R
(R,(V \ a)) + (R,a) is Element of the carrier of R
the addF of R . ((R,(V \ a)),(R,a)) is Element of the carrier of R
[(R,(V \ a)),(R,a)] is set
{(R,(V \ a)),(R,a)} is finite set
{(R,(V \ a))} is non empty trivial finite 1 -element set
{{(R,(V \ a)),(R,a)},{(R,(V \ a))}} is finite V42() set
the addF of R . [(R,(V \ a)),(R,a)] is set
(R,((V \ a) /\ a)) is Element of the carrier of R
((R,(V \ a)) + (R,a)) - (R,((V \ a) /\ a)) is Element of the carrier of R
- (R,((V \ a) /\ a)) is Element of the carrier of R
((R,(V \ a)) + (R,a)) + (- (R,((V \ a) /\ a))) is Element of the carrier of R
the addF of R . (((R,(V \ a)) + (R,a)),(- (R,((V \ a) /\ a)))) is Element of the carrier of R
[((R,(V \ a)) + (R,a)),(- (R,((V \ a) /\ a)))] is set
{((R,(V \ a)) + (R,a)),(- (R,((V \ a) /\ a)))} is finite set
{((R,(V \ a)) + (R,a))} is non empty trivial finite 1 -element set
{{((R,(V \ a)) + (R,a)),(- (R,((V \ a) /\ a)))},{((R,(V \ a)) + (R,a))}} is finite V42() set
the addF of R . [((R,(V \ a)) + (R,a)),(- (R,((V \ a) /\ a)))] is set
0. R is V57(R) Element of the carrier of R
the ZeroF of R is Element of the carrier of R
((R,(V \ a)) + (R,a)) - (0. R) is Element of the carrier of R
- (0. R) is Element of the carrier of R
((R,(V \ a)) + (R,a)) + (- (0. R)) is Element of the carrier of R
the addF of R . (((R,(V \ a)) + (R,a)),(- (0. R))) is Element of the carrier of R
[((R,(V \ a)) + (R,a)),(- (0. R))] is set
{((R,(V \ a)) + (R,a)),(- (0. R))} is finite set
{{((R,(V \ a)) + (R,a)),(- (0. R))},{((R,(V \ a)) + (R,a))}} is finite V42() set
the addF of R . [((R,(V \ a)) + (R,a)),(- (0. R))] 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
bool the carrier of R is non empty set
V is finite Element of bool the carrier of R
a is finite Element of bool the carrier of R
V \ a is finite Element of bool the carrier of R
(R,(V \ a)) is Element of the carrier of R
(R,V) is Element of the carrier of R
V /\ a is finite Element of bool the carrier of R
(R,(V /\ a)) is Element of the carrier of R
(R,V) - (R,(V /\ a)) is Element of the carrier of R
- (R,(V /\ a)) is Element of the carrier of R
(R,V) + (- (R,(V /\ a))) 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 . ((R,V),(- (R,(V /\ a)))) is Element of the carrier of R
[(R,V),(- (R,(V /\ a)))] is set
{(R,V),(- (R,(V /\ a)))} is finite set
{(R,V)} is non empty trivial finite 1 -element set
{{(R,V),(- (R,(V /\ a)))},{(R,V)}} is finite V42() set
the addF of R . [(R,V),(- (R,(V /\ a)))] is set
V \ (V /\ a) is finite Element of bool the carrier of R
V \/ (V /\ a) is finite Element of bool the carrier of R
(R,(V \/ (V /\ a))) is Element of the carrier of R
(R,(V \/ (V /\ a))) - (R,(V /\ a)) is Element of the carrier of R
(R,(V \/ (V /\ a))) + (- (R,(V /\ a))) is Element of the carrier of R
the addF of R . ((R,(V \/ (V /\ a))),(- (R,(V /\ a)))) is Element of the carrier of R
[(R,(V \/ (V /\ a))),(- (R,(V /\ a)))] is set
{(R,(V \/ (V /\ a))),(- (R,(V /\ a)))} is finite set
{(R,(V \/ (V /\ a)))} is non empty trivial finite 1 -element set
{{(R,(V \/ (V /\ a))),(- (R,(V /\ a)))},{(R,(V \/ (V /\ a)))}} is finite V42() set
the addF of R . [(R,(V \/ (V /\ a))),(- (R,(V /\ a)))] 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
bool the carrier of R is non empty set
V is finite Element of bool the carrier of R
a is finite Element of bool the carrier of R
V \+\ a is finite Element of bool the carrier of R
V \ a is finite set
a \ V is finite set
(V \ a) \/ (a \ V) is finite set
(R,(V \+\ a)) is Element of the carrier of R
V \/ a is finite Element of bool the carrier of R
(R,(V \/ a)) is Element of the carrier of R
V /\ a is finite Element of bool the carrier of R
(R,(V /\ a)) is Element of the carrier of R
(R,(V \/ a)) - (R,(V /\ a)) is Element of the carrier of R
- (R,(V /\ a)) is Element of the carrier of R
(R,(V \/ a)) + (- (R,(V /\ a))) 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 . ((R,(V \/ a)),(- (R,(V /\ a)))) is Element of the carrier of R
[(R,(V \/ a)),(- (R,(V /\ a)))] is set
{(R,(V \/ a)),(- (R,(V /\ a)))} is finite set
{(R,(V \/ a))} is non empty trivial finite 1 -element set
{{(R,(V \/ a)),(- (R,(V /\ a)))},{(R,(V \/ a))}} is finite V42() set
the addF of R . [(R,(V \/ a)),(- (R,(V /\ a)))] is set
(V \/ a) \ (V /\ a) is finite Element of bool the carrier of R
(V \/ a) /\ (V /\ a) is finite Element of bool the carrier of R
(R,((V \/ a) /\ (V /\ a))) is Element of the carrier of R
(R,(V \/ a)) - (R,((V \/ a) /\ (V /\ a))) is Element of the carrier of R
- (R,((V \/ a) /\ (V /\ a))) is Element of the carrier of R
(R,(V \/ a)) + (- (R,((V \/ a) /\ (V /\ a)))) is Element of the carrier of R
the addF of R . ((R,(V \/ a)),(- (R,((V \/ a) /\ (V /\ a))))) is Element of the carrier of R
[(R,(V \/ a)),(- (R,((V \/ a) /\ (V /\ a))))] is set
{(R,(V \/ a)),(- (R,((V \/ a) /\ (V /\ a))))} is finite set
{{(R,(V \/ a)),(- (R,((V \/ a) /\ (V /\ a))))},{(R,(V \/ a))}} is finite V42() set
the addF of R . [(R,(V \/ a)),(- (R,((V \/ a) /\ (V /\ a))))] is set
(V \/ a) /\ V is finite Element of bool the carrier of R
((V \/ a) /\ V) /\ a is finite Element of bool the carrier of R
(R,(((V \/ a) /\ V) /\ a)) is Element of the carrier of R
(R,(V \/ a)) - (R,(((V \/ a) /\ V) /\ a)) is Element of the carrier of R
- (R,(((V \/ a) /\ V) /\ a)) is Element of the carrier of R
(R,(V \/ a)) + (- (R,(((V \/ a) /\ V) /\ a))) is Element of the carrier of R
the addF of R . ((R,(V \/ a)),(- (R,(((V \/ a) /\ V) /\ a)))) is Element of the carrier of R
[(R,(V \/ a)),(- (R,(((V \/ a) /\ V) /\ a)))] is set
{(R,(V \/ a)),(- (R,(((V \/ a) /\ V) /\ a)))} is finite set
{{(R,(V \/ a)),(- (R,(((V \/ a) /\ V) /\ a)))},{(R,(V \/ a))}} is finite V42() set
the addF of R . [(R,(V \/ a)),(- (R,(((V \/ a) /\ V) /\ a)))] is set
R is non empty Abelian add-associative right_zeroed V108() addLoopStr
the carrier of R is non empty set
bool the carrier of R is non empty set
V is finite Element of bool the carrier of R
a is finite Element of bool the carrier of R
V \+\ a is finite Element of bool the carrier of R
V \ a is finite set
a \ V is finite set
(V \ a) \/ (a \ V) is finite set
(R,(V \+\ a)) is Element of the carrier of R
V \ a is finite Element of bool the carrier of R
(R,(V \ a)) is Element of the carrier of R
a \ V is finite Element of bool the carrier of R
(R,(a \ V)) is Element of the carrier of R
(R,(V \ a)) + (R,(a \ 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 . ((R,(V \ a)),(R,(a \ V))) is Element of the carrier of R
[(R,(V \ a)),(R,(a \ V))] is set
{(R,(V \ a)),(R,(a \ V))} is finite set
{(R,(V \ a))} is non empty trivial finite 1 -element set
{{(R,(V \ a)),(R,(a \ V))},{(R,(V \ a))}} is finite V42() set
the addF of R . [(R,(V \ a)),(R,(a \ V))] is set
R is non empty ZeroStr
the carrier of R is non empty set
Funcs ( the carrier of R,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of R, REAL
bool the carrier of R is non empty set
the carrier of R --> 0 is Relation-like the carrier of R -defined REAL -valued RAT -valued INT -valued Function-like non empty total quasi_total V112() V113() V114() V115() Element of bool [: the carrier of R,REAL:]
[: the carrier of R,REAL:] is non empty non trivial non finite V112() V113() V114() set
bool [: the carrier of R,REAL:] is non empty non trivial non finite set
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() Element of Funcs ( the carrier of R,REAL)
{} 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
V is Element of the carrier of R
a . V is ext-real V36() real Element of REAL
R is non empty addLoopStr
the carrier of R is non empty set
Funcs ( the carrier of R,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of R, REAL
R is non empty addLoopStr
the carrier of R is non empty set
Funcs ( the carrier of R,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of R, REAL
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() Element of Funcs ( the carrier of R,REAL)
support a is set
dom a is Element of bool the carrier of R
bool the carrier of R is non empty set
V is set
R is non empty addLoopStr
the carrier of R is non empty set
Funcs ( the carrier of R,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of R, REAL
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() Element of Funcs ( the carrier of R,REAL)
support a is set
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not a . b₁ = 0 } is set
V is Element of bool the carrier of R
w is set
a . w is ext-real V36() real set
w is set
I is Element of the carrier of R
a . I is ext-real V36() real Element of REAL
w is set
I is Element of the carrier of R
a . I is ext-real V36() real Element of REAL
w is set
a . w is ext-real V36() real set
R is non empty addLoopStr
the carrier of R is non empty set
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a) is Element of bool the carrier of R
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not a . b₁ = 0 } is set
v is finite Element of bool the carrier of R
u is set
w is Element of the carrier of R
a . w is ext-real V36() real Element of REAL
R is non empty addLoopStr
the carrier of R is non empty set
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a) is finite Element of bool the carrier of R
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not a . b₁ = 0 } is set
V is Element of the carrier of R
a . V is ext-real V36() real Element of REAL
v is Element of the carrier of R
a . v is ext-real V36() real Element of REAL
R is non empty addLoopStr
the carrier of R is non empty set
[: the carrier of R,REAL:] is non empty non trivial non finite V112() V113() V114() set
bool [: the carrier of R,REAL:] is non empty non trivial non finite set
the carrier of R --> 0 is Relation-like the carrier of R -defined REAL -valued RAT -valued INT -valued Function-like non empty total quasi_total V112() V113() V114() V115() Element of bool [: the carrier of R,REAL:]
Funcs ( the carrier of R,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of R, REAL
a is Relation-like the carrier of R -defined REAL -valued Function-like non empty total quasi_total V112() V113() V114() Element of bool [: the carrier of R,REAL:]
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() Element of Funcs ( the carrier of R,REAL)
bool the carrier of R is non empty set
{} 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
v 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
u is Element of the carrier of R
V . u is ext-real V36() real Element of REAL
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,v) is finite Element of bool the carrier of R
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not v . b₁ = 0 } is set
the Element of { b₁ where b₁ is Element of the carrier of R : not v . b₁ = 0 } is Element of { b₁ where b₁ is Element of the carrier of R : not v . b₁ = 0 }
I is Element of the carrier of R
v . I is ext-real V36() real Element of REAL
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a) is finite Element of bool the carrier of R
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not a . b₁ = 0 } is set
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not V . b₁ = 0 } is set
v is set
u is Element of the carrier of R
V . u is ext-real V36() real Element of REAL
a . u is ext-real V36() real Element of REAL
a . v is ext-real V36() real set
V . v is ext-real V36() real set
R is non empty addLoopStr
the carrier of R is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
a is Element of the carrier of R
(R) . a is ext-real V36() real Element of REAL
(R,(R)) is finite Element of bool the carrier of R
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not (R) . b₁ = 0 } 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 Element of bool the carrier of R
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not V . b₁ = 0 } 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
bool the carrier of R is non empty set
a is Element of bool the carrier of R
V is Element of bool the carrier of R
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,a)
(R,v) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not v . b₁ = 0 } 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
bool the carrier of R is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
a is Element of bool the carrier of R
(R,(R)) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not (R) . b₁ = 0 } 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
{} the carrier of 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
bool the carrier of R is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R, {} the carrier of R)
(R,a) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not a . b₁ = 0 } 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
[: the carrier of R,REAL:] is non empty non trivial non finite V112() V113() V114() set
bool [: the carrier of R,REAL:] is non empty non trivial non finite 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 the carrier of R -defined REAL -valued Function-like non empty total quasi_total V112() V113() V114() Element of bool [: the carrier of R,REAL:]
v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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
rng v is finite set
u is set
w is set
v . w is set
Seg (len a) is finite len a -element V122() V123() V124() V125() V126() V127() Element of bool NAT
I is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
v . I is set
a /. I is Element of the carrier of R
V . (a /. I) is ext-real V36() real Element of REAL
(V . (a /. I)) * (a /. I) 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 . ((V . (a /. I)),(a /. I)) is set
[(V . (a /. I)),(a /. I)] is set
{(V . (a /. I)),(a /. I)} is finite set
{(V . (a /. I))} is non empty trivial finite 1 -element V122() V123() V124() set
{{(V . (a /. I)),(a /. I)},{(V . (a /. I))}} is finite V42() set
the Mult of R . [(V . (a /. I)),(a /. I)] is set
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 u 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
a /. w is Element of the carrier of R
V . (a /. w) is ext-real V36() real Element of REAL
(V . (a /. w)) * (a /. w) 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 . ((V . (a /. w)),(a /. w)) is set
[(V . (a /. w)),(a /. w)] is set
{(V . (a /. w)),(a /. w)} is finite set
{(V . (a /. w))} is non empty trivial finite 1 -element V122() V123() V124() set
{{(V . (a /. w)),(a /. w)},{(V . (a /. w))}} is finite V42() set
the Mult of R . [(V . (a /. w)),(a /. w)] 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
dom v is finite V122() V123() V124() V125() V126() V127() Element of bool 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 u is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
w is ext-real ordinal natural V36() real finite cardinal set
Seg (len v) is finite len v -element V122() V123() V124() V125() V126() V127() Element of bool NAT
v . w is set
a /. w is Element of the carrier of R
V . (a /. w) is ext-real V36() real Element of REAL
(V . (a /. w)) * (a /. w) 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 . ((V . (a /. w)),(a /. w)) is set
[(V . (a /. w)),(a /. w)] is set
{(V . (a /. w)),(a /. w)} is finite set
{(V . (a /. w))} is non empty trivial finite 1 -element V122() V123() V124() set
{{(V . (a /. w)),(a /. w)},{(V . (a /. w))}} is finite V42() set
the Mult of R . [(V . (a /. w)),(a /. w)] is set
u . w is set
R is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
a 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 a is non empty set
[: the carrier of a,REAL:] is non empty non trivial non finite V112() V113() V114() set
bool [: the carrier of a,REAL:] is non empty non trivial non finite set
V is Element of the carrier of a
v is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a
dom v is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
v . R is set
u is Relation-like the carrier of a -defined REAL -valued Function-like non empty total quasi_total V112() V113() V114() Element of bool [: the carrier of a,REAL:]
(a,v,u) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a
(a,v,u) . R is set
u . V is ext-real V36() real Element of REAL
(u . V) * V is Element of the carrier of a
the Mult of a is Relation-like [:REAL, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of a:], the carrier of a:]
[:REAL, the carrier of a:] is non empty non trivial non finite set
[:[:REAL, the carrier of a:], the carrier of a:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of a:], the carrier of a:] is non empty non trivial non finite set
the Mult of a . ((u . V),V) is set
[(u . V),V] is set
{(u . V),V} is finite set
{(u . V)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(u . V),V},{(u . V)}} is finite V42() set
the Mult of a . [(u . V),V] is set
v /. R is Element of the carrier of a
len (a,v,u) 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 (a,v,u) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
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
[: the carrier of R,REAL:] is non empty non trivial non finite V112() V113() V114() set
bool [: the carrier of R,REAL:] is non empty non trivial non finite set
<*> 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 FinSequence-membered M12( the carrier of R)
a is Relation-like the carrier of R -defined REAL -valued Function-like non empty total quasi_total V112() V113() V114() Element of bool [: the carrier of R,REAL:]
(R,(<*> 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 (R,(<*> the carrier of R),a) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
len (<*> the carrier of R) is Function-like functional empty ext-real ordinal natural V36() real finite V42() cardinal {} -element FinSequence-membered V110() V111() V122() V123() V124() V125() V126() V127() V128() Element of NAT
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
[: the carrier of R,REAL:] is non empty non trivial non finite V112() V113() V114() set
bool [: the carrier of R,REAL:] is non empty non trivial non finite set
a is Element of the carrier of R
<*a*> 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)
V is Relation-like the carrier of R -defined REAL -valued Function-like non empty total quasi_total V112() V113() V114() Element of bool [: the carrier of R,REAL:]
(R,<*a*>,V) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
V . a is ext-real V36() real Element of REAL
(V . a) * a 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 . ((V . a),a) is set
[(V . a),a] is set
{(V . a),a} is finite set
{(V . a)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(V . a),a},{(V . a)}} is finite V42() set
the Mult of R . [(V . a),a] is set
<*((V . a) * a)*> 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))
{1} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() Element of bool REAL
len (R,<*a*>,V) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
len <*a*> is non empty ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom (R,<*a*>,V) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
(R,<*a*>,V) . 1 is set
<*a*> /. 1 is Element of the carrier of R
V . (<*a*> /. 1) is ext-real V36() real Element of REAL
(V . (<*a*> /. 1)) * (<*a*> /. 1) is Element of the carrier of R
the Mult of R . ((V . (<*a*> /. 1)),(<*a*> /. 1)) is set
[(V . (<*a*> /. 1)),(<*a*> /. 1)] is set
{(V . (<*a*> /. 1)),(<*a*> /. 1)} is finite set
{(V . (<*a*> /. 1))} is non empty trivial finite 1 -element V122() V123() V124() set
{{(V . (<*a*> /. 1)),(<*a*> /. 1)},{(V . (<*a*> /. 1))}} is finite V42() set
the Mult of R . [(V . (<*a*> /. 1)),(<*a*> /. 1)] is set
(V . (<*a*> /. 1)) * a is Element of the carrier of R
the Mult of R . ((V . (<*a*> /. 1)),a) is set
[(V . (<*a*> /. 1)),a] is set
{(V . (<*a*> /. 1)),a} is finite set
{{(V . (<*a*> /. 1)),a},{(V . (<*a*> /. 1))}} is finite V42() set
the Mult of R . [(V . (<*a*> /. 1)),a] 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
[: the carrier of R,REAL:] is non empty non trivial non finite V112() V113() V114() set
bool [: the carrier of R,REAL:] is non empty non trivial non finite set
a is Element of the carrier of R
V is Element of the carrier of R
<*a,V*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R
v is Relation-like the carrier of R -defined REAL -valued Function-like non empty total quasi_total V112() V113() V114() Element of bool [: the carrier of R,REAL:]
(R,<*a,V*>,v) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
v . a is ext-real V36() real Element of REAL
(v . a) * a 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 . ((v . a),a) is set
[(v . a),a] is set
{(v . a),a} is finite set
{(v . a)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(v . a),a},{(v . a)}} is finite V42() set
the Mult of R . [(v . a),a] is set
v . V is ext-real V36() real Element of REAL
(v . V) * V is Element of the carrier of R
the Mult of R . ((v . V),V) is set
[(v . V),V] is set
{(v . V),V} is finite set
{(v . V)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(v . V),V},{(v . V)}} is finite V42() set
the Mult of R . [(v . V),V] is set
<*((v . a) * a),((v . V) * V)*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len (R,<*a,V*>,v) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
len <*a,V*> is non empty ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom (R,<*a,V*>,v) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
{1,2} is finite V42() V122() V123() V124() V125() V126() V127() Element of bool REAL
(R,<*a,V*>,v) . 2 is set
<*a,V*> /. 2 is Element of the carrier of R
v . (<*a,V*> /. 2) is ext-real V36() real Element of REAL
(v . (<*a,V*> /. 2)) * (<*a,V*> /. 2) is Element of the carrier of R
the Mult of R . ((v . (<*a,V*> /. 2)),(<*a,V*> /. 2)) is set
[(v . (<*a,V*> /. 2)),(<*a,V*> /. 2)] is set
{(v . (<*a,V*> /. 2)),(<*a,V*> /. 2)} is finite set
{(v . (<*a,V*> /. 2))} is non empty trivial finite 1 -element V122() V123() V124() set
{{(v . (<*a,V*> /. 2)),(<*a,V*> /. 2)},{(v . (<*a,V*> /. 2))}} is finite V42() set
the Mult of R . [(v . (<*a,V*> /. 2)),(<*a,V*> /. 2)] is set
(v . (<*a,V*> /. 2)) * V is Element of the carrier of R
the Mult of R . ((v . (<*a,V*> /. 2)),V) is set
[(v . (<*a,V*> /. 2)),V] is set
{(v . (<*a,V*> /. 2)),V} is finite set
{{(v . (<*a,V*> /. 2)),V},{(v . (<*a,V*> /. 2))}} is finite V42() set
the Mult of R . [(v . (<*a,V*> /. 2)),V] is set
(R,<*a,V*>,v) . 1 is set
<*a,V*> /. 1 is Element of the carrier of R
v . (<*a,V*> /. 1) is ext-real V36() real Element of REAL
(v . (<*a,V*> /. 1)) * (<*a,V*> /. 1) is Element of the carrier of R
the Mult of R . ((v . (<*a,V*> /. 1)),(<*a,V*> /. 1)) is set
[(v . (<*a,V*> /. 1)),(<*a,V*> /. 1)] is set
{(v . (<*a,V*> /. 1)),(<*a,V*> /. 1)} is finite set
{(v . (<*a,V*> /. 1))} is non empty trivial finite 1 -element V122() V123() V124() set
{{(v . (<*a,V*> /. 1)),(<*a,V*> /. 1)},{(v . (<*a,V*> /. 1))}} is finite V42() set
the Mult of R . [(v . (<*a,V*> /. 1)),(<*a,V*> /. 1)] is set
(v . (<*a,V*> /. 1)) * a is Element of the carrier of R
the Mult of R . ((v . (<*a,V*> /. 1)),a) is set
[(v . (<*a,V*> /. 1)),a] is set
{(v . (<*a,V*> /. 1)),a} is finite set
{{(v . (<*a,V*> /. 1)),a},{(v . (<*a,V*> /. 1))}} is finite V42() set
the Mult of R . [(v . (<*a,V*> /. 1)),a] 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
[: the carrier of R,REAL:] is non empty non trivial non finite V112() V113() V114() set
bool [: the carrier of R,REAL:] is non empty non trivial non finite set
a is Element of the carrier of R
V is Element of the carrier of R
v is Element of the carrier of R
<*a,V,v*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R
u is Relation-like the carrier of R -defined REAL -valued Function-like non empty total quasi_total V112() V113() V114() Element of bool [: the carrier of R,REAL:]
(R,<*a,V,v*>,u) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
u . a is ext-real V36() real Element of REAL
(u . a) * a 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 . ((u . a),a) is set
[(u . a),a] is set
{(u . a),a} is finite set
{(u . a)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(u . a),a},{(u . a)}} is finite V42() set
the Mult of R . [(u . a),a] is set
u . V is ext-real V36() real Element of REAL
(u . V) * V is Element of the carrier of R
the Mult of R . ((u . V),V) is set
[(u . V),V] is set
{(u . V),V} is finite set
{(u . V)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(u . V),V},{(u . V)}} is finite V42() set
the Mult of R . [(u . V),V] is set
u . v is ext-real V36() real Element of REAL
(u . v) * v is Element of the carrier of R
the Mult of R . ((u . v),v) is set
[(u . v),v] is set
{(u . v),v} is finite set
{(u . v)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(u . v),v},{(u . v)}} is finite V42() set
the Mult of R . [(u . v),v] is set
<*((u . a) * a),((u . V) * V),((u . v) * v)*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len (R,<*a,V,v*>,u) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
len <*a,V,v*> is non empty ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
dom (R,<*a,V,v*>,u) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
{1,2,3} is non empty finite V122() V123() V124() V125() V126() V127() Element of bool REAL
(R,<*a,V,v*>,u) . 3 is set
<*a,V,v*> /. 3 is Element of the carrier of R
u . (<*a,V,v*> /. 3) is ext-real V36() real Element of REAL
(u . (<*a,V,v*> /. 3)) * (<*a,V,v*> /. 3) is Element of the carrier of R
the Mult of R . ((u . (<*a,V,v*> /. 3)),(<*a,V,v*> /. 3)) is set
[(u . (<*a,V,v*> /. 3)),(<*a,V,v*> /. 3)] is set
{(u . (<*a,V,v*> /. 3)),(<*a,V,v*> /. 3)} is finite set
{(u . (<*a,V,v*> /. 3))} is non empty trivial finite 1 -element V122() V123() V124() set
{{(u . (<*a,V,v*> /. 3)),(<*a,V,v*> /. 3)},{(u . (<*a,V,v*> /. 3))}} is finite V42() set
the Mult of R . [(u . (<*a,V,v*> /. 3)),(<*a,V,v*> /. 3)] is set
(u . (<*a,V,v*> /. 3)) * v is Element of the carrier of R
the Mult of R . ((u . (<*a,V,v*> /. 3)),v) is set
[(u . (<*a,V,v*> /. 3)),v] is set
{(u . (<*a,V,v*> /. 3)),v} is finite set
{{(u . (<*a,V,v*> /. 3)),v},{(u . (<*a,V,v*> /. 3))}} is finite V42() set
the Mult of R . [(u . (<*a,V,v*> /. 3)),v] is set
(R,<*a,V,v*>,u) . 2 is set
<*a,V,v*> /. 2 is Element of the carrier of R
u . (<*a,V,v*> /. 2) is ext-real V36() real Element of REAL
(u . (<*a,V,v*> /. 2)) * (<*a,V,v*> /. 2) is Element of the carrier of R
the Mult of R . ((u . (<*a,V,v*> /. 2)),(<*a,V,v*> /. 2)) is set
[(u . (<*a,V,v*> /. 2)),(<*a,V,v*> /. 2)] is set
{(u . (<*a,V,v*> /. 2)),(<*a,V,v*> /. 2)} is finite set
{(u . (<*a,V,v*> /. 2))} is non empty trivial finite 1 -element V122() V123() V124() set
{{(u . (<*a,V,v*> /. 2)),(<*a,V,v*> /. 2)},{(u . (<*a,V,v*> /. 2))}} is finite V42() set
the Mult of R . [(u . (<*a,V,v*> /. 2)),(<*a,V,v*> /. 2)] is set
(u . (<*a,V,v*> /. 2)) * V is Element of the carrier of R
the Mult of R . ((u . (<*a,V,v*> /. 2)),V) is set
[(u . (<*a,V,v*> /. 2)),V] is set
{(u . (<*a,V,v*> /. 2)),V} is finite set
{{(u . (<*a,V,v*> /. 2)),V},{(u . (<*a,V,v*> /. 2))}} is finite V42() set
the Mult of R . [(u . (<*a,V,v*> /. 2)),V] is set
(R,<*a,V,v*>,u) . 1 is set
<*a,V,v*> /. 1 is Element of the carrier of R
u . (<*a,V,v*> /. 1) is ext-real V36() real Element of REAL
(u . (<*a,V,v*> /. 1)) * (<*a,V,v*> /. 1) is Element of the carrier of R
the Mult of R . ((u . (<*a,V,v*> /. 1)),(<*a,V,v*> /. 1)) is set
[(u . (<*a,V,v*> /. 1)),(<*a,V,v*> /. 1)] is set
{(u . (<*a,V,v*> /. 1)),(<*a,V,v*> /. 1)} is finite set
{(u . (<*a,V,v*> /. 1))} is non empty trivial finite 1 -element V122() V123() V124() set
{{(u . (<*a,V,v*> /. 1)),(<*a,V,v*> /. 1)},{(u . (<*a,V,v*> /. 1))}} is finite V42() set
the Mult of R . [(u . (<*a,V,v*> /. 1)),(<*a,V,v*> /. 1)] is set
(u . (<*a,V,v*> /. 1)) * a is Element of the carrier of R
the Mult of R . ((u . (<*a,V,v*> /. 1)),a) is set
[(u . (<*a,V,v*> /. 1)),a] is set
{(u . (<*a,V,v*> /. 1)),a} is finite set
{{(u . (<*a,V,v*> /. 1)),a},{(u . (<*a,V,v*> /. 1))}} is finite V42() set
the Mult of R . [(u . (<*a,V,v*> /. 1)),a] 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 Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a) is finite Element of bool the carrier of R
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not a . b₁ = 0 } is set
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
(R,v,a) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (R,v,a) is Element of the carrier of R
rng v is finite Element of bool the carrier of R
V is Element of the carrier of R
v 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
rng u is finite Element of bool the carrier of R
(R,u,a) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (R,u,a) 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
(R,w,a) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (R,w,a) is Element 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
dom u is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
len u is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
Seg (len u) is finite len u -element V122() V123() V124() V125() V126() V127() Element of bool NAT
I is set
w . I is set
{(w . I)} is non empty trivial finite 1 -element set
u " {(w . I)} is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
k is set
{k} is non empty trivial finite 1 -element set
[:(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
I is Relation-like dom u -defined dom u -valued Function-like total quasi_total finite V112() V113() V114() V115() Element of bool [:(dom u),(dom u):]
k is set
dom I is finite set
I . k is ext-real ordinal natural V36() real finite cardinal set
y is set
I . y is ext-real ordinal natural V36() real finite cardinal set
dom I is finite V122() V123() V124() V125() V126() V127() Element of bool (dom u)
bool (dom u) is non empty finite V42() set
w . k is set
{(w . k)} is non empty trivial finite 1 -element set
w . y is set
{(w . y)} is non empty trivial finite 1 -element set
u " {(w . k)} is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
{(I . k)} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() set
u " {(w . y)} is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
{(I . y)} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() set
len (R,u,a) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
rng I is finite V122() V123() V124() V125() V126() V127() Element of bool (dom u)
bool (dom u) is non empty finite V42() set
y is set
u . y is set
v is set
w . v is set
{(w . v)} is non empty trivial finite 1 -element set
u " {(w . v)} is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
Im (u,y) is set
{y} is non empty trivial finite 1 -element set
u .: {y} is finite set
u " (Im (u,y)) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
I . v is ext-real ordinal natural V36() real finite cardinal set
{(I . v)} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() set
dom I is finite V122() V123() V124() V125() V126() V127() Element of bool (dom u)
dom (R,u,a) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
Seg (len (R,u,a)) is finite len (R,u,a) -element V122() V123() V124() V125() V126() V127() Element of bool NAT
[:(dom (R,u,a)),(dom (R,u,a)):] is RAT -valued INT -valued finite V112() V113() V114() V115() set
bool [:(dom (R,u,a)),(dom (R,u,a)):] is non empty finite V42() set
y 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):]
dom (R,w,a) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
len (R,w,a) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
Seg (len (R,w,a)) is finite len (R,w,a) -element V122() V123() V124() V125() V126() V127() Element of bool NAT
v2 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w . v2 is set
(R,w,a) . v2 is set
w /. v2 is Element of the carrier of R
a . (w /. v2) is ext-real V36() real Element of REAL
(a . (w /. v2)) * (w /. v2) 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 . (w /. v2)),(w /. v2)) is set
[(a . (w /. v2)),(w /. v2)] is set
{(a . (w /. v2)),(w /. v2)} is finite set
{(a . (w /. v2))} is non empty trivial finite 1 -element V122() V123() V124() set
{{(a . (w /. v2)),(w /. v2)},{(a . (w /. v2))}} is finite V42() set
the Mult of R . [(a . (w /. v2)),(w /. v2)] is set
v is Relation-like dom (R,u,a) -defined dom (R,u,a) -valued Function-like one-to-one total quasi_total onto bijective finite V112() V113() V114() V115() Element of bool [:(dom (R,u,a)),(dom (R,u,a)):]
dom v is finite V122() V123() V124() V125() V126() V127() Element of bool (dom (R,u,a))
bool (dom (R,u,a)) is non empty finite V42() set
v . v2 is ext-real ordinal natural V36() real finite cardinal set
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
u . (v . v2) is set
{(u . (v . v2))} is non empty trivial finite 1 -element set
Im (u,(v . v2)) is set
{(v . v2)} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() set
u .: {(v . v2)} is finite set
{(w . v2)} is non empty trivial finite 1 -element set
u " {(w . v2)} is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
u .: (u " {(w . v2)}) is finite Element of bool the carrier of R
n is Element of the carrier of R
u is Element of the carrier of R
u /. w is Element of the carrier of R
(R,u,a) . (v . v2) 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
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
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
(R,(R)) is finite Element of bool the carrier of R
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not (R) . b₁ = 0 } 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
rng a is finite Element of bool the carrier of R
(R,a,(R)) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (R,a,(R)) is Element 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
len (R,a,(R)) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
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
bool the carrier of R is non empty set
a is Element of bool the carrier of R
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,a)
(R,V) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not V . b₁ = 0 } is set
card (R,V) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of omega
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V) 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
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,a)
(R,V) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not V . b₁ = 0 } is set
card (R,V) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of omega
(R,V) 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
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,a)
(R,v) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not v . b₁ = 0 } is set
(R,v) 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
rng u is finite Element of bool the carrier of R
(R,u,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 (R,u,v) is Element of the carrier of R
Seg V is finite V -element V122() V123() V124() V125() V126() V127() Element of bool NAT
u | (Seg V) 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
card (R,v) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of omega
V + 1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
len u is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
len (R,u,v) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
Seg (V + 1) is finite V + 1 -element V122() V123() V124() V125() V126() V127() Element of bool NAT
dom u is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
u . (V + 1) is set
[: the carrier of R,REAL:] is non empty non trivial non finite V112() V113() V114() set
bool [: the carrier of R,REAL:] is non empty non trivial non finite set
I is Element of the carrier of R
k is Relation-like the carrier of R -defined REAL -valued Function-like non empty total quasi_total V112() V113() V114() Element of bool [: the carrier of R,REAL:]
k . I is ext-real V36() real Element of REAL
Funcs ( the carrier of R,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of R, REAL
v is Element of the carrier of R
y is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() Element of Funcs ( the carrier of R,REAL)
y . v is ext-real V36() real Element of REAL
v . v is ext-real V36() real Element of REAL
{I} is non empty trivial finite 1 -element Element of bool the carrier of R
a \ {I} is Element of bool the carrier of R
v . I is ext-real V36() real Element of REAL
(v . I) * I 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 . ((v . I),I) is set
[(v . I),I] is set
{(v . I),I} is finite set
{(v . I)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(v . I),I},{(v . I)}} is finite V42() set
the Mult of R . [(v . I),I] is set
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,v) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not v . b₁ = 0 } is set
(R,v) \ {I} is finite Element of bool the carrier of R
v1 is set
v2 is Element of the carrier of R
v . v2 is ext-real V36() real Element of REAL
v . v2 is ext-real V36() real Element of REAL
v1 is set
v2 is Element of the carrier of R
v . v2 is ext-real V36() real Element of REAL
v . v2 is ext-real V36() real Element of REAL
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
v1 is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,a)
(R,w,v1) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len (R,w,v1) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
rng w is finite Element of bool the carrier of R
(R,v1) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not v1 . b₁ = 0 } is set
v2 is set
dom w is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
n is set
w . n is set
w is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w . w is set
u . w is set
v2 is set
n is set
u . n is set
w is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
(dom u) \ (Seg V) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
(Seg (V + 1)) \ (Seg V) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
{(V + 1)} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() Element of bool REAL
(dom u) /\ (Seg V) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
dom w is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
w . w is set
u . w is set
(Seg (V + 1)) /\ (Seg V) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
dom (R,w,v1) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
dom (R,u,v) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
(dom (R,u,v)) /\ (Seg V) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
v2 is set
n is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
u . n is set
dom w is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
w . n is set
u is Element of the carrier of R
(R,w,v1) . n is set
v1 . u is ext-real V36() real Element of REAL
(v1 . u) * u is Element of the carrier of R
the Mult of R . ((v1 . u),u) is set
[(v1 . u),u] is set
{(v1 . u),u} is finite set
{(v1 . u)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(v1 . u),u},{(v1 . u)}} is finite V42() set
the Mult of R . [(v1 . u),u] is set
v . u is ext-real V36() real Element of REAL
(v . u) * u is Element of the carrier of R
the Mult of R . ((v . u),u) is set
[(v . u),u] is set
{(v . u),u} is finite set
{(v . u)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(v . u),u},{(v . u)}} is finite V42() set
the Mult of R . [(v . u),u] is set
w is Element of the carrier of R
(R,w,v1) . v2 is set
(R,u,v) . v2 is set
(R,u,v) | (Seg V) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of R:]
card (R,v1) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of omega
card {I} is non empty ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of omega
(V + 1) - (card {I}) is ext-real V36() real Element of REAL
(V + 1) - 1 is ext-real V36() real Element of REAL
(R,v1) is Element of the carrier of R
Sum (R,w,v1) is Element of the carrier of R
Seg (len (R,w,v1)) is finite len (R,w,v1) -element V122() V123() V124() V125() V126() V127() Element of bool NAT
(R,u,v) . (len u) is set
(Sum (R,w,v1)) + ((v . I) * I) 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 (R,w,v1)),((v . I) * I)) is Element of the carrier of R
[(Sum (R,w,v1)),((v . I) * I)] is set
{(Sum (R,w,v1)),((v . I) * I)} is finite set
{(Sum (R,w,v1))} is non empty trivial finite 1 -element set
{{(Sum (R,w,v1)),((v . I) * I)},{(Sum (R,w,v1))}} is finite V42() set
the addF of R . [(Sum (R,w,v1)),((v . I) * I)] is set
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 the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,a)
(R,v) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not v . b₁ = 0 } is set
card (R,v) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of omega
V + 1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
(R,v) is Element of the carrier of R
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,a)
(R,V) is Element of the carrier of R
(R,V) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not V . b₁ = 0 } is set
card (R,V) is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of omega
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(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
V is ext-real V36() real Element of REAL
v is Element of the carrier of R
V * 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 . (V,v) is set
[V,v] is set
{V,v} is finite set
{V} is non empty trivial finite 1 -element V122() V123() V124() set
{{V,v},{V}} is finite V42() set
the Mult of R . [V,v] is set
[: the carrier of R,REAL:] is non empty non trivial non finite V112() V113() V114() set
bool [: the carrier of R,REAL:] is non empty non trivial non finite set
u is Relation-like the carrier of R -defined REAL -valued Function-like non empty total quasi_total V112() V113() V114() Element of bool [: the carrier of R,REAL:]
u . v is ext-real V36() real Element of REAL
Funcs ( the carrier of R,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of R, REAL
I is Element of the carrier of R
{v} is non empty trivial finite 1 -element Element of bool the carrier of R
w is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() Element of Funcs ( the carrier of R,REAL)
w . I is ext-real V36() real Element of REAL
I is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,I) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not I . b₁ = 0 } is set
k is set
y is Element of the carrier of R
I . y is ext-real V36() real Element of REAL
k is set
k is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,a)
(R,k) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not k . b₁ = 0 } is set
(R,k) is Element of the carrier of R
y is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
rng y is finite Element of bool the carrier of R
(R,y,k) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (R,y,k) 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)
k . v is ext-real V36() real Element of REAL
(k . v) * v is Element of the carrier of R
the Mult of R . ((k . v),v) is set
[(k . v),v] is set
{(k . v),v} is finite set
{(k . v)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(k . v),v},{(k . v)}} is finite V42() set
the Mult of R . [(k . v),v] is set
<*((k . v) * 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))
V is Element of the carrier of R
v is Element of the carrier of R
V + 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 . (V,v) is Element of the carrier of R
[V,v] is set
{V,v} is finite set
{V} is non empty trivial finite 1 -element set
{{V,v},{V}} is finite V42() set
the addF of R . [V,v] is set
1 * 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 . (1,V) is set
[1,V] is set
{1,V} is finite set
{{1,V},{1}} is finite V42() set
the Mult of R . [1,V] is set
(1 * V) + V is Element of the carrier of R
the addF of R . ((1 * V),V) is Element of the carrier of R
[(1 * V),V] is set
{(1 * V),V} is finite set
{(1 * V)} is non empty trivial finite 1 -element set
{{(1 * V),V},{(1 * V)}} is finite V42() set
the addF of R . [(1 * V),V] is set
(1 * V) + (1 * V) is Element of the carrier of R
the addF of R . ((1 * V),(1 * V)) is Element of the carrier of R
[(1 * V),(1 * V)] is set
{(1 * V),(1 * V)} is finite set
{{(1 * V),(1 * V)},{(1 * V)}} is finite V42() set
the addF of R . [(1 * V),(1 * V)] is set
1 + 1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
(1 + 1) * V is Element of the carrier of R
the Mult of R . ((1 + 1),V) is set
[(1 + 1),V] is set
{(1 + 1),V} is finite set
{(1 + 1)} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() set
{{(1 + 1),V},{(1 + 1)}} is finite V42() set
the Mult of R . [(1 + 1),V] is set
2 * V is Element of the carrier of R
the Mult of R . (2,V) is set
[2,V] is set
{2,V} is finite set
{2} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() set
{{2,V},{2}} is finite V42() set
the Mult of R . [2,V] is set
[: the carrier of R,REAL:] is non empty non trivial non finite V112() V113() V114() set
bool [: the carrier of R,REAL:] is non empty non trivial non finite set
u is Relation-like the carrier of R -defined REAL -valued Function-like non empty total quasi_total V112() V113() V114() Element of bool [: the carrier of R,REAL:]
u . V is ext-real V36() real Element of REAL
u . v is ext-real V36() real Element of REAL
Funcs ( the carrier of R,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of R, REAL
I is Element of the carrier of R
{V,v} is finite Element of bool the carrier of R
w is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() Element of Funcs ( the carrier of R,REAL)
w . I is ext-real V36() real Element of REAL
I is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,I) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not I . b₁ = 0 } is set
k is set
y is Element of the carrier of R
I . y is ext-real V36() real Element of REAL
k is set
1 * 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 . (1,v) is set
[1,v] is set
{1,v} is finite set
{{1,v},{1}} is finite V42() set
the Mult of R . [1,v] is set
1 * V is Element of the carrier of R
the Mult of R . (1,V) is set
[1,V] is set
{1,V} is finite set
{{1,V},{1}} is finite V42() set
the Mult of R . [1,V] is set
k is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,a)
(R,k) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not k . b₁ = 0 } is set
(R,k) is Element of the carrier of R
y is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
rng y is finite Element of bool the carrier of R
(R,y,k) is Relation-like NAT -defined the carrier of R -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (R,y,k) is Element of the carrier of R
<*V,v*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R
<*v,V*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R
<*(1 * V),(1 * v)*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R
<*(1 * v),(1 * V)*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R
v is Element of the carrier of R
V is ext-real V36() real Element of REAL
V * 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 . (V,v) is set
[V,v] is set
{V,v} is finite set
{V} is non empty trivial finite 1 -element V122() V123() V124() set
{{V,v},{V}} is finite V42() set
the Mult of R . [V,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
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
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
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
{} the carrier of 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
bool the carrier of R is non empty 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 the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R, {} the carrier of R)
(R,a) is Element of the carrier of R
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
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 Element of the carrier of R
{a} is non empty trivial finite 1 -element Element of bool the carrier of R
bool the carrier of R is non empty set
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,{a})
(R,V) is Element of the carrier of R
V . a is ext-real V36() real Element of REAL
(V . a) * a 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 . ((V . a),a) is set
[(V . a),a] is set
{(V . a),a} is finite set
{(V . a)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(V . a),a},{(V . a)}} is finite V42() set
the Mult of R . [(V . a),a] is set
(R,V) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not V . b₁ = 0 } is set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
0. R is V57(R) Element of the carrier of R
the ZeroF of R is Element of the carrier of R
0 * a is Element of the carrier of R
the Mult of R . (0,a) is set
[0,a] is set
{0,a} is finite set
{0} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() set
{{0,a},{0}} is finite V42() set
the Mult of R . [0,a] 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
rng v is finite Element of bool the carrier of R
(R,v,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 (R,v,V) is Element of the carrier of R
<*a*> 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)
<*((V . a) * a)*> 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))
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 Element of the carrier of R
V is Element of the carrier of R
{a,V} is finite Element of bool the carrier of R
bool the carrier of R is non empty set
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,{a,V})
(R,v) is Element of the carrier of R
v . a is ext-real V36() real Element of REAL
(v . a) * a 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 . ((v . a),a) is set
[(v . a),a] is set
{(v . a),a} is finite set
{(v . a)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(v . a),a},{(v . a)}} is finite V42() set
the Mult of R . [(v . a),a] is set
v . V is ext-real V36() real Element of REAL
(v . V) * V is Element of the carrier of R
the Mult of R . ((v . V),V) is set
[(v . V),V] is set
{(v . V),V} is finite set
{(v . V)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(v . V),V},{(v . V)}} is finite V42() set
the Mult of R . [(v . V),V] is set
((v . a) * a) + ((v . V) * 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 . (((v . a) * a),((v . V) * V)) is Element of the carrier of R
[((v . a) * a),((v . V) * V)] is set
{((v . a) * a),((v . V) * V)} is finite set
{((v . a) * a)} is non empty trivial finite 1 -element set
{{((v . a) * a),((v . V) * V)},{((v . a) * a)}} is finite V42() set
the addF of R . [((v . a) * a),((v . V) * V)] is set
(R,v) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not v . b₁ = 0 } is set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
0. R is V57(R) Element of the carrier of R
the ZeroF of R is Element of the carrier of R
(0. R) + (0. R) is Element of the carrier of R
the addF of R . ((0. R),(0. R)) is Element of the carrier of R
[(0. R),(0. R)] is set
{(0. R),(0. R)} is finite set
{(0. R)} is non empty trivial finite 1 -element set
{{(0. R),(0. R)},{(0. R)}} is finite V42() set
the addF of R . [(0. R),(0. R)] is set
0 * a is Element of the carrier of R
the Mult of R . (0,a) is set
[0,a] is set
{0,a} is finite set
{0} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() set
{{0,a},{0}} is finite V42() set
the Mult of R . [0,a] is set
(0 * a) + (0. R) is Element of the carrier of R
the addF of R . ((0 * a),(0. R)) is Element of the carrier of R
[(0 * a),(0. R)] is set
{(0 * a),(0. R)} is finite set
{(0 * a)} is non empty trivial finite 1 -element set
{{(0 * a),(0. R)},{(0 * a)}} is finite V42() set
the addF of R . [(0 * a),(0. R)] is set
0 * V is Element of the carrier of R
the Mult of R . (0,V) is set
[0,V] is set
{0,V} is finite set
{{0,V},{0}} is finite V42() set
the Mult of R . [0,V] is set
(0 * a) + (0 * V) is Element of the carrier of R
the addF of R . ((0 * a),(0 * V)) is Element of the carrier of R
[(0 * a),(0 * V)] is set
{(0 * a),(0 * V)} is finite set
{{(0 * a),(0 * V)},{(0 * a)}} is finite V42() set
the addF of R . [(0 * a),(0 * V)] is set
((v . a) * a) + (0 * V) is Element of the carrier of R
the addF of R . (((v . a) * a),(0 * V)) is Element of the carrier of R
[((v . a) * a),(0 * V)] is set
{((v . a) * a),(0 * V)} is finite set
{{((v . a) * a),(0 * V)},{((v . a) * a)}} is finite V42() set
the addF of R . [((v . a) * a),(0 * V)] is set
{a} is non empty trivial finite 1 -element Element of bool the carrier of R
u is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,{a})
(R,u) 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
((v . a) * a) + (0. R) is Element of the carrier of R
the addF of R . (((v . a) * a),(0. R)) is Element of the carrier of R
[((v . a) * a),(0. R)] is set
{((v . a) * a),(0. R)} is finite set
{{((v . a) * a),(0. R)},{((v . a) * a)}} is finite V42() set
the addF of R . [((v . a) * a),(0. R)] is set
0 * V is Element of the carrier of R
the Mult of R . (0,V) is set
[0,V] is set
{0,V} is finite set
{0} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() set
{{0,V},{0}} is finite V42() set
the Mult of R . [0,V] is set
((v . a) * a) + (0 * V) is Element of the carrier of R
the addF of R . (((v . a) * a),(0 * V)) is Element of the carrier of R
[((v . a) * a),(0 * V)] is set
{((v . a) * a),(0 * V)} is finite set
{{((v . a) * a),(0 * V)},{((v . a) * a)}} is finite V42() set
the addF of R . [((v . a) * a),(0 * V)] is set
{V} is non empty trivial finite 1 -element Element of bool the carrier of R
u is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,{V})
(R,u) 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
(0. R) + ((v . V) * V) is Element of the carrier of R
the addF of R . ((0. R),((v . V) * V)) is Element of the carrier of R
[(0. R),((v . V) * V)] is set
{(0. R),((v . V) * V)} is finite set
{(0. R)} is non empty trivial finite 1 -element set
{{(0. R),((v . V) * V)},{(0. R)}} is finite V42() set
the addF of R . [(0. R),((v . V) * V)] is set
0 * a is Element of the carrier of R
the Mult of R . (0,a) is set
[0,a] is set
{0,a} is finite set
{0} is non empty trivial finite V42() 1 -element V122() V123() V124() V125() V126() V127() set
{{0,a},{0}} is finite V42() set
the Mult of R . [0,a] is set
(0 * a) + ((v . V) * V) is Element of the carrier of R
the addF of R . ((0 * a),((v . V) * V)) is Element of the carrier of R
[(0 * a),((v . V) * V)] is set
{(0 * a),((v . V) * V)} is finite set
{(0 * a)} is non empty trivial finite 1 -element set
{{(0 * a),((v . V) * V)},{(0 * a)}} is finite V42() set
the addF of R . [(0 * a),((v . V) * V)] is set
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
(R,u,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 (R,u,v) is Element of the carrier of R
<*a,V*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R
<*V,a*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R
<*((v . a) * a),((v . V) * V)*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R
<*((v . V) * V),((v . a) * a)*> is Relation-like NAT -defined the carrier of R -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of R
{a} is non empty trivial finite 1 -element Element of bool the carrier of R
{V} is non empty trivial finite 1 -element Element of bool the carrier of R
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
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 the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a) is finite Element of bool the carrier of R
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not a . b₁ = 0 } is set
(R,a) is Element of the carrier of R
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
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 Element of the carrier of R
{a} is non empty trivial finite 1 -element Element of bool the carrier of R
bool the carrier of R is non empty set
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not V . b₁ = 0 } is set
(R,V) is Element of the carrier of R
V . a is ext-real V36() real Element of REAL
(V . a) * a 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 . ((V . a),a) is set
[(V . a),a] is set
{(V . a),a} is finite set
{(V . a)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(V . a),a},{(V . a)}} is finite V42() set
the Mult of R . [(V . a),a] 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 Element of the carrier of R
V is Element of the carrier of R
{a,V} is finite Element of bool the carrier of R
bool the carrier of R is non empty set
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,v) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not v . b₁ = 0 } is set
(R,v) is Element of the carrier of R
v . a is ext-real V36() real Element of REAL
(v . a) * a 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 . ((v . a),a) is set
[(v . a),a] is set
{(v . a),a} is finite set
{(v . a)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(v . a),a},{(v . a)}} is finite V42() set
the Mult of R . [(v . a),a] is set
v . V is ext-real V36() real Element of REAL
(v . V) * V is Element of the carrier of R
the Mult of R . ((v . V),V) is set
[(v . V),V] is set
{(v . V),V} is finite set
{(v . V)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(v . V),V},{(v . V)}} is finite V42() set
the Mult of R . [(v . V),V] is set
((v . a) * a) + ((v . V) * 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 . (((v . a) * a),((v . V) * V)) is Element of the carrier of R
[((v . a) * a),((v . V) * V)] is set
{((v . a) * a),((v . V) * V)} is finite set
{((v . a) * a)} is non empty trivial finite 1 -element set
{{((v . a) * a),((v . V) * V)},{((v . a) * a)}} is finite V42() set
the addF of R . [((v . a) * a),((v . V) * V)] is set
R is non empty addLoopStr
the carrier of R is non empty set
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
v is Element of the carrier of R
a . v is ext-real V36() real Element of REAL
V . v is ext-real V36() real Element of REAL
R is non empty addLoopStr
the carrier of R is non empty set
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
a + V is Relation-like the carrier of R -defined Function-like total V112() V113() V114() set
Funcs ( the carrier of R,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of R, REAL
a + V is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like non empty total total quasi_total V112() V113() V114() Element of bool [: the carrier of R,REAL:]
[: the carrier of R,REAL:] is non empty non trivial non finite V112() V113() V114() set
bool [: the carrier of R,REAL:] is non empty non trivial non finite set
u is Element of the carrier of R
(R,a) is finite Element of bool the carrier of R
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not a . b₁ = 0 } is set
(R,V) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not V . b₁ = 0 } is set
(R,a) \/ (R,V) is finite Element of bool the carrier of R
V . u is ext-real V36() real Element of REAL
a . u is ext-real V36() real Element of REAL
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() Element of Funcs ( the carrier of R,REAL)
v . u is ext-real V36() real Element of REAL
0 + 0 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
a + V is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like non empty total total quasi_total V112() V113() V114() Element of bool [: the carrier of R,REAL:]
[: the carrier of R,REAL:] is non empty non trivial non finite V112() V113() V114() set
bool [: the carrier of R,REAL:] is non empty non trivial non finite set
u is Element of the carrier of R
v . u is ext-real V36() real Element of REAL
a . u is ext-real V36() real Element of REAL
V . u is ext-real V36() real Element of REAL
(a . u) + (V . u) is ext-real V36() real Element of REAL
u is Element of the carrier of R
v . u is ext-real V36() real set
(a + V) . u is ext-real V36() real set
v . u is ext-real V36() real Element of REAL
a . u is ext-real V36() real Element of REAL
V . u is ext-real V36() real Element of REAL
(a . u) + (V . u) is ext-real V36() real Element of REAL
(a + V) . u is ext-real V36() real Element of REAL
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 Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a) is finite Element of bool the carrier of R
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not a . b₁ = 0 } is set
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,V) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(R,(R,a,V)) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not (R,a,V) . b₁ = 0 } is set
(R,V) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not V . b₁ = 0 } is set
(R,a) \/ (R,V) is finite Element of bool the carrier of R
v is set
u is Element of the carrier of R
(R,a,V) . u is ext-real V36() real Element of REAL
a . u is ext-real V36() real Element of REAL
V . u is ext-real V36() real Element of REAL
(a . u) + (V . u) is ext-real V36() real Element of REAL
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
bool the carrier of R is non empty set
a is Element of bool the carrier of R
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V,v) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(R,V) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not V . b₁ = 0 } is set
(R,v) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not v . b₁ = 0 } is set
(R,V) \/ (R,v) is finite Element of bool the carrier of R
(R,(R,V,v)) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not (R,V,v) . b₁ = 0 } is set
R is non empty addLoopStr
the carrier of R is non empty set
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,V) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(R,V,a) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
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 Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,V) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V,v) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(R,a,(R,V,v)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(R,(R,a,V),v) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
u is Element of the carrier of R
(R,a,(R,V,v)) . u is ext-real V36() real Element of REAL
(R,(R,a,V),v) . u is ext-real V36() real Element of REAL
a . u is ext-real V36() real Element of REAL
(R,V,v) . u is ext-real V36() real Element of REAL
(a . u) + ((R,V,v) . u) is ext-real V36() real Element of REAL
V . u is ext-real V36() real Element of REAL
v . u is ext-real V36() real Element of REAL
(V . u) + (v . u) is ext-real V36() real Element of REAL
(a . u) + ((V . u) + (v . u)) is ext-real V36() real Element of REAL
(a . u) + (V . u) is ext-real V36() real Element of REAL
((a . u) + (V . u)) + (v . u) is ext-real V36() real Element of REAL
(R,a,V) . u is ext-real V36() real Element of REAL
((R,a,V) . u) + (v . u) is ext-real V36() real Element of REAL
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
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,(R)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(R,(R),a) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
V is Element of the carrier of R
(R,a,(R)) . V is ext-real V36() real Element of REAL
a . V is ext-real V36() real Element of REAL
(R) . V is ext-real V36() real Element of REAL
(a . V) + ((R) . V) is ext-real V36() real Element of REAL
(a . V) + 0 is ext-real V36() real Element of REAL
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 the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
[: the carrier of R,REAL:] is non empty non trivial non finite V112() V113() V114() set
bool [: the carrier of R,REAL:] is non empty non trivial non finite set
v is Relation-like the carrier of R -defined REAL -valued Function-like non empty total quasi_total V112() V113() V114() Element of bool [: the carrier of R,REAL:]
Funcs ( the carrier of R,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of R, REAL
w is Element of the carrier of R
(R,V) is finite Element of bool the carrier of R
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not V . b₁ = 0 } is set
V . w is ext-real V36() real Element of REAL
u is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() Element of Funcs ( the carrier of R,REAL)
u . w is ext-real V36() real Element of REAL
a * 0 is ext-real V36() real Element of REAL
w is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
I is Element of the carrier of R
w . I is ext-real V36() real Element of REAL
V . I is ext-real V36() real Element of REAL
a * (V . I) is ext-real V36() real Element of REAL
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
u is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
w is Element of the carrier of R
v . w is ext-real V36() real Element of REAL
u . w is ext-real V36() real Element of REAL
V . w is ext-real V36() real Element of REAL
a * (V . w) is ext-real V36() real Element of REAL
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 the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R,a,V)) is finite Element of bool the carrier of R
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not (R,a,V) . b₁ = 0 } is set
(R,V) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not V . b₁ = 0 } is set
w is set
I is Element of the carrier of R
(R,a,V) . I is ext-real V36() real Element of REAL
V . I is ext-real V36() real Element of REAL
a * (V . I) is ext-real V36() real Element of REAL
w is set
I is Element of the carrier of R
V . I is ext-real V36() real Element of REAL
(R,a,V) . I is ext-real V36() real Element of REAL
a * (V . I) is ext-real V36() real Element of REAL
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
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,0,a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V is Element of the carrier of R
(R,0,a) . V is ext-real V36() real Element of REAL
(R) . V is ext-real V36() real Element of REAL
a . V is ext-real V36() real Element of REAL
0 * (a . V) is ext-real V36() real Element of REAL
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
bool the carrier of R is non empty set
a is ext-real V36() real Element of REAL
V is Element of bool the carrier of R
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R,a,v)) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not (R,a,v) . b₁ = 0 } is set
(R,v) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not v . b₁ = 0 } 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 ext-real V36() real Element of REAL
a + V is ext-real V36() real Element of REAL
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(a + V),v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R,a,v),(R,V,v)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
u is Element of the carrier of R
(R,(a + V),v) . u is ext-real V36() real Element of REAL
(R,(R,a,v),(R,V,v)) . u is ext-real V36() real Element of REAL
v . u is ext-real V36() real Element of REAL
(a + V) * (v . u) is ext-real V36() real Element of REAL
a * (v . u) is ext-real V36() real Element of REAL
V * (v . u) is ext-real V36() real Element of REAL
(a * (v . u)) + (V * (v . u)) is ext-real V36() real Element of REAL
(R,a,v) . u is ext-real V36() real Element of REAL
((R,a,v) . u) + (V * (v . u)) is ext-real V36() real Element of REAL
(R,V,v) . u is ext-real V36() real Element of REAL
((R,a,v) . u) + ((R,V,v) . u) is ext-real V36() real Element of REAL
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 the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V,v) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(R,a,(R,V,v)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R,a,V),(R,a,v)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
u is Element of the carrier of R
(R,a,(R,V,v)) . u is ext-real V36() real Element of REAL
(R,(R,a,V),(R,a,v)) . u is ext-real V36() real Element of REAL
(R,V,v) . u is ext-real V36() real Element of REAL
a * ((R,V,v) . u) is ext-real V36() real Element of REAL
V . u is ext-real V36() real Element of REAL
v . u is ext-real V36() real Element of REAL
(V . u) + (v . u) is ext-real V36() real Element of REAL
a * ((V . u) + (v . u)) is ext-real V36() real Element of REAL
a * (V . u) is ext-real V36() real Element of REAL
a * (v . u) is ext-real V36() real Element of REAL
(a * (V . u)) + (a * (v . u)) is ext-real V36() real Element of REAL
(R,a,V) . u is ext-real V36() real Element of REAL
((R,a,V) . u) + (a * (v . u)) is ext-real V36() real Element of REAL
(R,a,v) . u is ext-real V36() real Element of REAL
((R,a,V) . u) + ((R,a,v) . u) is ext-real V36() real Element of REAL
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 ext-real V36() real Element of REAL
a * V is ext-real V36() real Element of REAL
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,(R,V,v)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(a * V),v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
u is Element of the carrier of R
(R,a,(R,V,v)) . u is ext-real V36() real Element of REAL
(R,(a * V),v) . u is ext-real V36() real Element of REAL
(R,V,v) . u is ext-real V36() real Element of REAL
a * ((R,V,v) . u) is ext-real V36() real Element of REAL
v . u is ext-real V36() real Element of REAL
V * (v . u) is ext-real V36() real Element of REAL
a * (V * (v . u)) is ext-real V36() real Element of REAL
(a * V) * (v . u) is ext-real V36() real Element of REAL
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 Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,1,a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V is Element of the carrier of R
(R,1,a) . V is ext-real V36() real Element of REAL
a . V is ext-real V36() real Element of REAL
1 * (a . V) is ext-real V36() real Element of REAL
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 Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
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 Element of the carrier of R
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V) . a is ext-real V36() real Element of REAL
V . a is ext-real V36() real Element of REAL
- (V . a) is ext-real V36() real Element of REAL
(- 1) * (V . a) is ext-real V36() real Element of REAL
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
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,V) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
v is Element of the carrier of R
V . v is ext-real V36() real Element of REAL
(R,a) . v is ext-real V36() real Element of REAL
a . v is ext-real V36() real Element of REAL
(a . v) + (V . v) is ext-real V36() real Element of REAL
(R) . v is ext-real V36() real Element of REAL
- (a . v) is ext-real V36() real Element of REAL
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 Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R,a)) is finite Element of bool the carrier of R
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not (R,a) . b₁ = 0 } is set
(R,a) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not a . b₁ = 0 } 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
bool the carrier of R is non empty set
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
a is Element of bool the carrier of R
(R,V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
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 Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R,a)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),(R,a)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V is Element of the carrier of R
(R,(R,a)) . V is ext-real V36() real Element of REAL
a . V is ext-real V36() real Element of REAL
(- 1) * (- 1) is ext-real V36() real Element of REAL
(R,((- 1) * (- 1)),a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,((- 1) * (- 1)),a) . V is ext-real V36() real Element of REAL
1 * (a . V) is ext-real V36() real Element of REAL
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 Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,(R,V)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
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 Element of the carrier of R
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V . a is ext-real V36() real Element of REAL
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V,(R,v)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(R,V,v) . a is ext-real V36() real Element of REAL
v . a is ext-real V36() real Element of REAL
(V . a) - (v . a) is ext-real V36() real Element of REAL
(R,v) . a is ext-real V36() real Element of REAL
(V . a) + ((R,v) . a) is ext-real V36() real Element of REAL
- (v . a) is ext-real V36() real Element of REAL
(V . a) + (- (v . a)) is ext-real V36() real Element of REAL
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 Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a) is finite Element of bool the carrier of R
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of the carrier of R : not a . b₁ = 0 } is set
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,(R,V)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(R,(R,a,V)) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not (R,a,V) . b₁ = 0 } is set
(R,V) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not V . b₁ = 0 } is set
(R,a) \/ (R,V) is finite Element of bool the carrier of R
(R,(R,V)) is finite Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : not (R,V) . b₁ = 0 } is set
(R,a) \/ (R,(R,V)) is finite Element of bool the carrier of R
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
bool the carrier of R is non empty set
a is Element of bool the carrier of R
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V,(R,v)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
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
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,(R,a)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
V is Element of the carrier of R
(R,a,a) . V is ext-real V36() real Element of REAL
(R) . V is ext-real V36() real Element of REAL
a . V is ext-real V36() real Element of REAL
(a . V) - (a . V) is ext-real V36() real Element of REAL
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
Funcs ( the carrier of R,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of R, REAL
a is set
V is set
a is set
V is set
v is set
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
(R) is set
the carrier of R is non empty set
the Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty set
a is Element of (R)
the carrier of R is non empty 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 Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R) is non empty set
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty set
[:(R),(R):] is non empty set
[:[:(R),(R):],(R):] is non empty set
bool [:[:(R),(R):],(R):] is non empty set
a is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
V is Element of (R)
(R,V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
the carrier of R is non empty set
v is Element of (R)
a . (V,v) is Element of (R)
[V,v] is set
{V,v} is finite set
{V} is non empty trivial finite 1 -element set
{{V,v},{V}} is finite V42() set
a . [V,v] is set
(R,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R,V),(R,v)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(R,(R,(R,V),(R,v))) is Element of (R)
a is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
V is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
v is Element of (R)
u is Element of (R)
a . (v,u) is Element of (R)
[v,u] is set
{v,u} is finite set
{v} is non empty trivial finite 1 -element set
{{v,u},{v}} is finite V42() set
a . [v,u] is set
(R,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
the carrier of R is non empty set
(R,u) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R,v),(R,u)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
V . (v,u) is Element of (R)
V . [v,u] 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
(R) is non empty set
[:REAL,(R):] is non empty non trivial non finite set
[:[:REAL,(R):],(R):] is non empty non trivial non finite set
bool [:[:REAL,(R):],(R):] is non empty non trivial non finite set
a is ext-real V36() real Element of REAL
V is Element of (R)
(R,V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
the carrier of R is non empty set
(R,a,(R,V)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R,a,(R,V))) is Element of (R)
a is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
V is ext-real V36() real Element of REAL
v is Element of (R)
[V,v] is Element of [:REAL,(R):]
{V,v} is finite set
{V} is non empty trivial finite 1 -element V122() V123() V124() set
{{V,v},{V}} is finite V42() set
a . [V,v] is Element of (R)
(R,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
the carrier of R is non empty set
(R,V,(R,v)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
a . (V,v) is Element of (R)
[V,v] is set
a . [V,v] is set
u is ext-real V36() real Element of REAL
(R,u,(R,v)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
a is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
V is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
v is ext-real V36() real Element of REAL
u is Element of (R)
a . (v,u) is Element of (R)
[v,u] is set
{v,u} is finite set
{v} is non empty trivial finite 1 -element V122() V123() V124() set
{{v,u},{v}} is finite V42() set
a . [v,u] is set
(R,u) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
the carrier of R is non empty set
(R,v,(R,u)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V . (v,u) is Element of (R)
V . [v,u] 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
(R) is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
the carrier of R is non empty set
(R,(R)) is Element of (R)
(R) is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
[:(R),(R):] is non empty set
[:[:(R),(R):],(R):] is non empty set
bool [:[:(R),(R):],(R):] is non empty set
(R) is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
[:REAL,(R):] is non empty non trivial non finite set
[:[:REAL,(R):],(R):] is non empty non trivial non finite set
bool [:[:REAL,(R):],(R):] is non empty non trivial non finite set
RLSStruct(# (R),(R,(R)),(R),(R) #) is non empty strict RLSStruct
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is RLSStruct
(R) is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
the carrier of R is non empty set
(R,(R)) is Element of (R)
(R) is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
[:(R),(R):] is non empty set
[:[:(R),(R):],(R):] is non empty set
bool [:[:(R),(R):],(R):] is non empty set
(R) is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
[:REAL,(R):] is non empty non trivial non finite set
[:[:REAL,(R):],(R):] is non empty non trivial non finite set
bool [:[:REAL,(R):],(R):] is non empty non trivial non finite set
RLSStruct(# (R),(R,(R)),(R),(R) #) is non empty strict RLSStruct
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty strict RLSStruct
(R) is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
the carrier of R is non empty set
(R,(R)) is Element of (R)
(R) is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
[:(R),(R):] is non empty set
[:[:(R),(R):],(R):] is non empty set
bool [:[:(R),(R):],(R):] is non empty set
(R) is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
[:REAL,(R):] is non empty non trivial non finite set
[:[:REAL,(R):],(R):] is non empty non trivial non finite set
bool [:[:REAL,(R):],(R):] is non empty non trivial non finite set
RLSStruct(# (R),(R,(R)),(R),(R) #) is non empty strict RLSStruct
the carrier of (R) is non empty set
u is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,u) is Element of (R)
(R,(R,u)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
w is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,w) is Element of (R)
(R,(R,w)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V is Element of the carrier of (R)
v is Element of the carrier of (R)
V + 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) . (V,v) is Element of the carrier of (R)
[V,v] is set
{V,v} is finite set
{V} is non empty trivial finite 1 -element set
{{V,v},{V}} is finite V42() set
the addF of (R) . [V,v] is set
(R,u,w) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
V is Element of the carrier of (R)
v is Element of the carrier of (R)
V + v is Element of the carrier of (R)
the addF of (R) . (V,v) is Element of the carrier of (R)
[V,v] is set
{V,v} is finite set
{V} is non empty trivial finite 1 -element set
{{V,v},{V}} is finite V42() set
the addF of (R) . [V,v] is set
v + V is Element of the carrier of (R)
the addF of (R) . (v,V) is Element of the carrier of (R)
[v,V] is set
{v,V} is finite set
{v} is non empty trivial finite 1 -element set
{{v,V},{v}} is finite V42() set
the addF of (R) . [v,V] is set
w is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
u is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,w,u) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
V is Element of the carrier of (R)
v is Element of the carrier of (R)
V + v is Element of the carrier of (R)
the addF of (R) . (V,v) is Element of the carrier of (R)
[V,v] is set
{V,v} is finite set
{V} is non empty trivial finite 1 -element set
{{V,v},{V}} is finite V42() set
the addF of (R) . [V,v] is set
u is Element of the carrier of (R)
(V + v) + u is Element of the carrier of (R)
the addF of (R) . ((V + v),u) is Element of the carrier of (R)
[(V + v),u] is set
{(V + v),u} is finite set
{(V + v)} is non empty trivial finite 1 -element set
{{(V + v),u},{(V + v)}} is finite V42() set
the addF of (R) . [(V + v),u] is set
v + u is Element of the carrier of (R)
the addF of (R) . (v,u) is Element of the carrier of (R)
[v,u] is set
{v,u} is finite set
{v} is non empty trivial finite 1 -element set
{{v,u},{v}} is finite V42() set
the addF of (R) . [v,u] is set
V + (v + u) is Element of the carrier of (R)
the addF of (R) . (V,(v + u)) is Element of the carrier of (R)
[V,(v + u)] is set
{V,(v + u)} is finite set
{{V,(v + u)},{V}} is finite V42() set
the addF of (R) . [V,(v + u)] is set
I is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
k is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,I,k) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
w is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,w,I) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(R,(R,w,I),k) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(R,w,(R,I,k)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
V 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)
V + (0. (R)) is Element of the carrier of (R)
the addF of (R) . (V,(0. (R))) is Element of the carrier of (R)
[V,(0. (R))] is set
{V,(0. (R))} is finite set
{V} is non empty trivial finite 1 -element set
{{V,(0. (R))},{V}} is finite V42() set
the addF of (R) . [V,(0. (R))] is set
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,v,(R)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
V is Element of the carrier of (R)
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
((R),(R,v)) is Element of the carrier of (R)
V + ((R),(R,v)) is Element of the carrier of (R)
the addF of (R) . (V,((R),(R,v))) is Element of the carrier of (R)
[V,((R),(R,v))] is set
{V,((R),(R,v))} is finite set
{V} is non empty trivial finite 1 -element set
{{V,((R),(R,v))},{V}} is finite V42() set
the addF of (R) . [V,((R),(R,v))] is set
(R,v,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,v,(R,v)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
0. (R) is V57((R)) Element of the carrier of (R)
the ZeroF of (R) is Element of the carrier of (R)
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,v) is Element of (R)
(R,(R,v)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V is Element of the carrier of (R)
u is ext-real V36() real Element of REAL
u * 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) . (u,V) is set
[u,V] is set
{u,V} is finite set
{u} is non empty trivial finite 1 -element V122() V123() V124() set
{{u,V},{u}} is finite V42() set
the Mult of (R) . [u,V] is set
(R,u,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V is ext-real V36() real set
v is Element of the carrier of (R)
u is Element of the carrier of (R)
v + u is Element of the carrier of (R)
the addF of (R) . (v,u) is Element of the carrier of (R)
[v,u] is set
{v,u} is finite set
{v} is non empty trivial finite 1 -element set
{{v,u},{v}} is finite V42() set
the addF of (R) . [v,u] is set
V * (v + u) is Element of the carrier of (R)
the Mult of (R) . (V,(v + u)) is set
[V,(v + u)] is set
{V,(v + u)} is finite set
{V} is non empty trivial finite 1 -element V122() V123() V124() set
{{V,(v + u)},{V}} is finite V42() set
the Mult of (R) . [V,(v + u)] is set
V * v is Element of the carrier of (R)
the Mult of (R) . (V,v) is set
[V,v] is set
{V,v} is finite set
{{V,v},{V}} is finite V42() set
the Mult of (R) . [V,v] is set
V * u is Element of the carrier of (R)
the Mult of (R) . (V,u) is set
[V,u] is set
{V,u} is finite set
{{V,u},{V}} is finite V42() set
the Mult of (R) . [V,u] is set
(V * v) + (V * u) is Element of the carrier of (R)
the addF of (R) . ((V * v),(V * u)) is Element of the carrier of (R)
[(V * v),(V * u)] is set
{(V * v),(V * u)} is finite set
{(V * v)} is non empty trivial finite 1 -element set
{{(V * v),(V * u)},{(V * v)}} is finite V42() set
the addF of (R) . [(V * v),(V * u)] is set
k is ext-real V36() real Element of REAL
k * v is Element of the carrier of (R)
the Mult of (R) . (k,v) is set
[k,v] is set
{k,v} is finite set
{k} is non empty trivial finite 1 -element V122() V123() V124() set
{{k,v},{k}} is finite V42() set
the Mult of (R) . [k,v] is set
w is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,k,w) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
k * u is Element of the carrier of (R)
the Mult of (R) . (k,u) is set
[k,u] is set
{k,u} is finite set
{{k,u},{k}} is finite V42() set
the Mult of (R) . [k,u] is set
I is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,k,I) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,w,I) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
k * (v + u) is Element of the carrier of (R)
the Mult of (R) . (k,(v + u)) is set
[k,(v + u)] is set
{k,(v + u)} is finite set
{{k,(v + u)},{k}} is finite V42() set
the Mult of (R) . [k,(v + u)] is set
(R,k,(R,w,I)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R,k,w),(R,k,I)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(k * v) + (k * u) is Element of the carrier of (R)
the addF of (R) . ((k * v),(k * u)) is Element of the carrier of (R)
[(k * v),(k * u)] is set
{(k * v),(k * u)} is finite set
{(k * v)} is non empty trivial finite 1 -element set
{{(k * v),(k * u)},{(k * v)}} is finite V42() set
the addF of (R) . [(k * v),(k * u)] is set
V is ext-real V36() real set
v is ext-real V36() real set
V + v is ext-real V36() real set
u is Element of the carrier of (R)
(V + v) * u is Element of the carrier of (R)
the Mult of (R) . ((V + v),u) is set
[(V + v),u] is set
{(V + v),u} is finite set
{(V + v)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(V + v),u},{(V + v)}} is finite V42() set
the Mult of (R) . [(V + v),u] is set
V * u is Element of the carrier of (R)
the Mult of (R) . (V,u) is set
[V,u] is set
{V,u} is finite set
{V} is non empty trivial finite 1 -element V122() V123() V124() set
{{V,u},{V}} is finite V42() set
the Mult of (R) . [V,u] is set
v * u is Element of the carrier of (R)
the Mult of (R) . (v,u) is set
[v,u] is set
{v,u} is finite set
{v} is non empty trivial finite 1 -element V122() V123() V124() set
{{v,u},{v}} is finite V42() set
the Mult of (R) . [v,u] is set
(V * u) + (v * u) is Element of the carrier of (R)
the addF of (R) . ((V * u),(v * u)) is Element of the carrier of (R)
[(V * u),(v * u)] is set
{(V * u),(v * u)} is finite set
{(V * u)} is non empty trivial finite 1 -element set
{{(V * u),(v * u)},{(V * u)}} is finite V42() set
the addF of (R) . [(V * u),(v * u)] is set
I is ext-real V36() real Element of REAL
I * u is Element of the carrier of (R)
the Mult of (R) . (I,u) is set
[I,u] is set
{I,u} is finite set
{I} is non empty trivial finite 1 -element V122() V123() V124() set
{{I,u},{I}} is finite V42() set
the Mult of (R) . [I,u] is set
w is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,I,w) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
k is ext-real V36() real Element of REAL
k * u is Element of the carrier of (R)
the Mult of (R) . (k,u) is set
[k,u] is set
{k,u} is finite set
{k} is non empty trivial finite 1 -element V122() V123() V124() set
{{k,u},{k}} is finite V42() set
the Mult of (R) . [k,u] is set
(R,k,w) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
I + k is ext-real V36() real Element of REAL
(I + k) * u is Element of the carrier of (R)
the Mult of (R) . ((I + k),u) is set
[(I + k),u] is set
{(I + k),u} is finite set
{(I + k)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(I + k),u},{(I + k)}} is finite V42() set
the Mult of (R) . [(I + k),u] is set
(R,(I + k),w) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R,I,w),(R,k,w)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(I * u) + (k * u) is Element of the carrier of (R)
the addF of (R) . ((I * u),(k * u)) is Element of the carrier of (R)
[(I * u),(k * u)] is set
{(I * u),(k * u)} is finite set
{(I * u)} is non empty trivial finite 1 -element set
{{(I * u),(k * u)},{(I * u)}} is finite V42() set
the addF of (R) . [(I * u),(k * u)] is set
V is ext-real V36() real set
v is ext-real V36() real set
V * v is ext-real V36() real set
u is Element of the carrier of (R)
(V * v) * u is Element of the carrier of (R)
the Mult of (R) . ((V * v),u) is set
[(V * v),u] is set
{(V * v),u} is finite set
{(V * v)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(V * v),u},{(V * v)}} is finite V42() set
the Mult of (R) . [(V * v),u] is set
v * u is Element of the carrier of (R)
the Mult of (R) . (v,u) is set
[v,u] is set
{v,u} is finite set
{v} is non empty trivial finite 1 -element V122() V123() V124() set
{{v,u},{v}} is finite V42() set
the Mult of (R) . [v,u] is set
V * (v * u) is Element of the carrier of (R)
the Mult of (R) . (V,(v * u)) is set
[V,(v * u)] is set
{V,(v * u)} is finite set
{V} is non empty trivial finite 1 -element V122() V123() V124() set
{{V,(v * u)},{V}} is finite V42() set
the Mult of (R) . [V,(v * u)] is set
k is ext-real V36() real Element of REAL
k * u is Element of the carrier of (R)
the Mult of (R) . (k,u) is set
[k,u] is set
{k,u} is finite set
{k} is non empty trivial finite 1 -element V122() V123() V124() set
{{k,u},{k}} is finite V42() set
the Mult of (R) . [k,u] is set
w is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,k,w) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
I is ext-real V36() real Element of REAL
I * k is ext-real V36() real Element of REAL
(I * k) * u is Element of the carrier of (R)
the Mult of (R) . ((I * k),u) is set
[(I * k),u] is set
{(I * k),u} is finite set
{(I * k)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(I * k),u},{(I * k)}} is finite V42() set
the Mult of (R) . [(I * k),u] is set
(R,(I * k),w) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,I,(R,k,w)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
I * (k * u) is Element of the carrier of (R)
the Mult of (R) . (I,(k * u)) is set
[I,(k * u)] is set
{I,(k * u)} is finite set
{I} is non empty trivial finite 1 -element V122() V123() V124() set
{{I,(k * u)},{I}} is finite V42() set
the Mult of (R) . [I,(k * u)] is set
V is Element of the carrier of (R)
1 * V is Element of the carrier of (R)
the Mult of (R) . (1,V) is set
[1,V] is set
{1,V} is finite set
{{1,V},{1}} is finite V42() set
the Mult of (R) . [1,V] is set
v is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,1,v) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
the carrier of R is non empty set
(R,(R)) is Element of (R)
(R) is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
[:(R),(R):] is non empty set
[:[:(R),(R):],(R):] is non empty set
bool [:[:(R),(R):],(R):] is non empty set
(R) is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
[:REAL,(R):] is non empty non trivial non finite set
[:[:REAL,(R):],(R):] is non empty non trivial non finite set
bool [:[:REAL,(R):],(R):] is non empty non trivial non finite set
RLSStruct(# (R),(R,(R)),(R),(R) #) is non empty strict RLSStruct
the carrier of (R) is non empty set
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
the carrier of R is non empty set
(R,(R)) is Element of (R)
(R) is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
[:(R),(R):] is non empty set
[:[:(R),(R):],(R):] is non empty set
bool [:[:(R),(R):],(R):] is non empty set
(R) is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
[:REAL,(R):] is non empty non trivial non finite set
[:[:REAL,(R):],(R):] is non empty non trivial non finite set
bool [:[:REAL,(R):],(R):] is non empty non trivial non finite set
RLSStruct(# (R),(R,(R)),(R),(R) #) is non empty strict RLSStruct
0. (R) is V57((R)) Element of the carrier of (R)
the carrier of (R) is non empty set
the ZeroF of (R) is Element of the carrier of (R)
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
the carrier of R is non empty set
(R,(R)) is Element of (R)
(R) is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
[:(R),(R):] is non empty set
[:[:(R),(R):],(R):] is non empty set
bool [:[:(R),(R):],(R):] is non empty set
(R) is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
[:REAL,(R):] is non empty non trivial non finite set
[:[:REAL,(R):],(R):] is non empty non trivial non finite set
bool [:[:REAL,(R):],(R):] is non empty non trivial non finite set
RLSStruct(# (R),(R,(R)),(R),(R) #) is non empty strict RLSStruct
the carrier of (R) is non empty set
[: the carrier of (R), the carrier of (R):] is non empty set
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):], 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
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
the carrier of R is non empty set
(R,(R)) is Element of (R)
(R) is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
[:(R),(R):] is non empty set
[:[:(R),(R):],(R):] is non empty set
bool [:[:(R),(R):],(R):] is non empty set
(R) is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
[:REAL,(R):] is non empty non trivial non finite set
[:[:REAL,(R):],(R):] is non empty non trivial non finite set
bool [:[:REAL,(R):],(R):] is non empty non trivial non finite set
RLSStruct(# (R),(R,(R)),(R),(R) #) is non empty strict RLSStruct
the carrier of (R) is non empty set
[:REAL, the carrier of (R):] is non empty non trivial non finite set
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):], 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
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
(R) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R)) is Element of (R)
(R) is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
[:(R),(R):] is non empty set
[:[:(R),(R):],(R):] is non empty set
bool [:[:(R),(R):],(R):] is non empty set
(R) is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
[:REAL,(R):] is non empty non trivial non finite set
[:[:REAL,(R):],(R):] is non empty non trivial non finite set
bool [:[:REAL,(R):],(R):] is non empty non trivial non finite set
RLSStruct(# (R),(R,(R)),(R),(R) #) is non empty strict RLSStruct
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
((R),a) is Element of the carrier of (R)
the carrier of (R) is non empty set
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
((R),V) is Element of the carrier of (R)
((R),a) + ((R),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) . (((R),a),((R),V)) is Element of the carrier of (R)
[((R),a),((R),V)] is set
{((R),a),((R),V)} is finite set
{((R),a)} is non empty trivial finite 1 -element set
{{((R),a),((R),V)},{((R),a)}} is finite V42() set
the addF of (R) . [((R),a),((R),V)] is set
(R,a,V) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
(R,a) is Element of (R)
(R,(R,a)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V) is Element of (R)
(R,(R,V)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
Funcs ( the carrier of R,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of R, REAL
[a,((R),V)] is Element of [:(Funcs ( the carrier of R,REAL)), the carrier of (R):]
[:(Funcs ( the carrier of R,REAL)), the carrier of (R):] is non empty set
{a,((R),V)} is finite set
{a} is functional non empty trivial finite 1 -element set
{{a,((R),V)},{a}} is finite V42() set
(R) . [a,((R),V)] is set
(R) . ((R,a),(R,V)) is Element of (R)
[(R,a),(R,V)] is set
{(R,a),(R,V)} is finite set
{(R,a)} is non empty trivial finite 1 -element set
{{(R,a),(R,V)},{(R,a)}} is finite V42() set
(R) . [(R,a),(R,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
(R) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R)) is Element of (R)
(R) is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
[:(R),(R):] is non empty set
[:[:(R),(R):],(R):] is non empty set
bool [:[:(R),(R):],(R):] is non empty set
(R) is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
[:REAL,(R):] is non empty non trivial non finite set
[:[:REAL,(R):],(R):] is non empty non trivial non finite set
bool [:[:REAL,(R):],(R):] is non empty non trivial non finite set
RLSStruct(# (R),(R,(R)),(R),(R) #) is non empty strict RLSStruct
a is ext-real V36() real Element of REAL
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
((R),V) is Element of the carrier of (R)
the carrier of (R) is non empty set
a * ((R),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,((R),V)) is set
[a,((R),V)] is set
{a,((R),V)} is finite set
{a} is non empty trivial finite 1 -element V122() V123() V124() set
{{a,((R),V)},{a}} is finite V42() set
the Mult of (R) . [a,((R),V)] is set
(R,a,V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V) is Element of (R)
(R,(R,V)) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
[a,(R,V)] is Element of [:REAL,(R):]
{a,(R,V)} is finite set
{{a,(R,V)},{a}} is finite V42() set
(R) . [a,(R,V)] is Element of (R)
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
(R) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R)) is Element of (R)
(R) is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
[:(R),(R):] is non empty set
[:[:(R),(R):],(R):] is non empty set
bool [:[:(R),(R):],(R):] is non empty set
(R) is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
[:REAL,(R):] is non empty non trivial non finite set
[:[:REAL,(R):],(R):] is non empty non trivial non finite set
bool [:[:REAL,(R):],(R):] is non empty non trivial non finite set
RLSStruct(# (R),(R,(R)),(R),(R) #) is non empty strict RLSStruct
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
((R),a) is Element of the carrier of (R)
the carrier of (R) is non empty set
- ((R),a) is Element of the carrier of (R)
(R,a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),a) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(- 1) * ((R),a) 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) . ((- 1),((R),a)) is set
[(- 1),((R),a)] is set
{(- 1),((R),a)} is finite set
{(- 1)} is non empty trivial finite 1 -element V122() V123() V124() set
{{(- 1),((R),a)},{(- 1)}} is finite V42() set
the Mult of (R) . [(- 1),((R),a)] 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
(R) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R)) is Element of (R)
(R) is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
[:(R),(R):] is non empty set
[:[:(R),(R):],(R):] is non empty set
bool [:[:(R),(R):],(R):] is non empty set
(R) is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
[:REAL,(R):] is non empty non trivial non finite set
[:[:REAL,(R):],(R):] is non empty non trivial non finite set
bool [:[:REAL,(R):],(R):] is non empty non trivial non finite set
RLSStruct(# (R),(R,(R)),(R),(R) #) is non empty strict RLSStruct
a is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
((R),a) is Element of the carrier of (R)
the carrier of (R) is non empty set
V is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
((R),V) is Element of the carrier of (R)
((R),a) - ((R),V) is Element of the carrier of (R)
- ((R),V) is Element of the carrier of (R)
((R),a) + (- ((R),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) . (((R),a),(- ((R),V))) is Element of the carrier of (R)
[((R),a),(- ((R),V))] is set
{((R),a),(- ((R),V))} is finite set
{((R),a)} is non empty trivial finite 1 -element set
{{((R),a),(- ((R),V))},{((R),a)}} is finite V42() set
the addF of (R) . [((R),a),(- ((R),V))] is set
(R,a,V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(- 1),V) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,a,(R,V)) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
((R),(R,V)) is Element of the carrier of (R)
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
bool the carrier of R is non empty set
(R) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() RLSStruct
(R) is non empty set
(R) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
(R,(R)) is Element of (R)
(R) is Relation-like [:(R),(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:(R),(R):],(R):]
[:(R),(R):] is non empty set
[:[:(R),(R):],(R):] is non empty set
bool [:[:(R),(R):],(R):] is non empty set
(R) is Relation-like [:REAL,(R):] -defined (R) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(R):],(R):]
[:REAL,(R):] is non empty non trivial non finite set
[:[:REAL,(R):],(R):] is non empty non trivial non finite set
bool [:[:REAL,(R):],(R):] is non empty non trivial non finite set
RLSStruct(# (R),(R,(R)),(R),(R) #) is non empty strict RLSStruct
a is Element of bool the carrier of R
{ b₁ where b₁ is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,a) : verum } is set
the carrier of (R) is non empty set
v is set
u is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,a)
bool the carrier of (R) is non empty set
v is Element of bool the carrier of (R)
u is Element of the carrier of (R)
w is Element of the carrier of (R)
u + w 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) . (u,w) is Element of the carrier of (R)
[u,w] is set
{u,w} is finite set
{u} is non empty trivial finite 1 -element set
{{u,w},{u}} is finite V42() set
the addF of (R) . [u,w] is set
I is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,a)
k is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,a)
((R),k) is Element of the carrier of (R)
((R),I) is Element of the carrier of (R)
(R,I,k) is Relation-like the carrier of R -defined the carrier of R -defined REAL -valued Function-like total total quasi_total V112() V113() V114() (R)
u is ext-real V36() real Element of REAL
w is Element of the carrier of (R)
u * w 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) . (u,w) is set
[u,w] is set
{u,w} is finite set
{u} is non empty trivial finite 1 -element V122() V123() V124() set
{{u,w},{u}} is finite V42() set
the Mult of (R) . [u,w] is set
I is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R,a)
((R),I) is Element of the carrier of (R)
u * ((R),I) is Element of the carrier of (R)
the Mult of (R) . (u,((R),I)) is set
[u,((R),I)] is set
{u,((R),I)} is finite set
{{u,((R),I)},{u}} is finite V42() set
the Mult of (R) . [u,((R),I)] is set
(R,u,I) is Relation-like the carrier of R -defined REAL -valued Function-like total quasi_total V112() V113() V114() (R)
V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() Subspace of (R)
the carrier of V is non empty set
v is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V108() Subspace of (R)
the carrier of v is non empty set
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() V133() associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of R is non empty set
a is Element of the carrier of R
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
the carrier of V is non empty set
v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
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 V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
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 v is Element of the carrier of V
Sum u is Element of the carrier of V
a * (Sum u) is Element of the carrier of V
w is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w + 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 V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len I is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
k is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len k 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
Sum I is Element of the carrier of V
Sum k is Element of the carrier of V
a * (Sum k) is Element of the carrier of V
Seg w is finite w -element V122() V123() V124() V125() V126() V127() Element of bool NAT
I | (Seg w) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of V:]
[:NAT, the carrier of V:] is non trivial non finite set
bool [:NAT, the carrier of V:] is non empty non trivial non finite set
k | (Seg w) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of V:]
v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
dom v is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
k | (dom v) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of V:]
y is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len y 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 y is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
v1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
v2 is Element of the carrier of V
v . v1 is set
k . v1 is set
I . v1 is set
a * v2 is Element of the carrier of V
y . v1 is set
Seg (w + 1) is finite w + 1 -element V122() V123() V124() V125() V126() V127() Element of bool NAT
dom k is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
I . (w + 1) is set
k . (w + 1) is set
v1 is Element of the carrier of V
v2 is Element of the carrier of V
a * v2 is Element of the carrier of V
I | (dom y) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of V:]
Sum y is Element of the carrier of V
(Sum y) + v1 is Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((Sum y),v1) is Element of the carrier of V
[(Sum y),v1] is set
{(Sum y),v1} is finite set
{(Sum y)} is non empty trivial finite 1 -element set
{{(Sum y),v1},{(Sum y)}} is finite V42() set
the addF of V . [(Sum y),v1] is set
Sum v is Element of the carrier of V
a * (Sum v) is Element of the carrier of V
(a * (Sum v)) + (a * v2) is Element of the carrier of V
the addF of V . ((a * (Sum v)),(a * v2)) is Element of the carrier of V
[(a * (Sum v)),(a * v2)] is set
{(a * (Sum v)),(a * v2)} is finite set
{(a * (Sum v))} is non empty trivial finite 1 -element set
{{(a * (Sum v)),(a * v2)},{(a * (Sum v))}} is finite V42() set
the addF of V . [(a * (Sum v)),(a * v2)] is set
(Sum v) + v2 is Element of the carrier of V
the addF of V . ((Sum v),v2) is Element of the carrier of V
[(Sum v),v2] is set
{(Sum v),v2} is finite set
{(Sum v)} is non empty trivial finite 1 -element set
{{(Sum v),v2},{(Sum v)}} is finite V42() set
the addF of V . [(Sum v),v2] is set
a * ((Sum v) + v2) is Element of the carrier of V
w is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len w 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 V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len I 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
Sum w is Element of the carrier of V
Sum I is Element of the carrier of V
a * (Sum I) is Element of the carrier of V
<*> the carrier of V is Relation-like NAT -defined the carrier of V -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 V,K353( the carrier of V))
K353( the carrier of V) is functional non empty FinSequence-membered M12( the carrier of V)
0. V is V57(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() V133() associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of R is non empty set
a is Element of the carrier of R
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
the carrier of V is non empty set
v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
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 V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
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 V
Sum v is Element of the carrier of V
a * (Sum v) is Element of the carrier of V
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
I is Element of the carrier of V
v . w is set
v /. w is Element of the carrier of V
u . w is set
a * I is Element of the carrier of V
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() V133() associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
a is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() VectSpStr over R
the carrier of a is non empty set
V is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a
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 a -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a
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 a -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a
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 a
Sum V is Element of the carrier of a
Sum v is Element of the carrier of a
(Sum V) - (Sum v) is Element of the carrier of a
- (Sum v) is Element of the carrier of a
(Sum V) + (- (Sum v)) is Element of the carrier of a
the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the addF of a . ((Sum V),(- (Sum v))) is Element of the carrier of a
[(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 a . [(Sum V),(- (Sum v))] is set
w is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len w 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
Seg (len v) is finite len v -element V122() V123() V124() V125() V126() V127() Element of bool NAT
I is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
w . I is set
v /. I is Element of the carrier of a
- (v /. I) is Element of the carrier of a
rng w is finite set
I is set
k is set
w . k is set
y is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
v /. y is Element of the carrier of a
- (v /. y) is Element of the carrier of a
v is Element of the carrier of a
dom v is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
k 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 a -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a
dom I is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
I . k is set
I /. k is Element of the carrier of a
u . k is set
V /. k is Element of the carrier of a
v /. k is Element of the carrier of a
(V /. k) - (v /. k) is Element of the carrier of a
- (v /. k) is Element of the carrier of a
(V /. k) + (- (v /. k)) is Element of the carrier of a
the addF of a . ((V /. k),(- (v /. k))) is Element of the carrier of a
[(V /. k),(- (v /. k))] is set
{(V /. k),(- (v /. k))} is finite set
{(V /. k)} is non empty trivial finite 1 -element set
{{(V /. k),(- (v /. k))},{(V /. k)}} is finite V42() set
the addF of a . [(V /. k),(- (v /. k))] is set
(V /. k) + (- (v /. k)) is Element of the carrier of a
(V /. k) + (I /. k) is Element of the carrier of a
the addF of a . ((V /. k),(I /. k)) is Element of the carrier of a
[(V /. k),(I /. k)] is set
{(V /. k),(I /. k)} is finite set
{{(V /. k),(I /. k)},{(V /. k)}} is finite V42() set
the addF of a . [(V /. k),(I /. k)] is set
Sum I is Element of the carrier of a
(Sum V) + (Sum I) is Element of the carrier of a
the addF of a . ((Sum V),(Sum I)) is Element of the carrier of a
[(Sum V),(Sum I)] is set
{(Sum V),(Sum I)} is finite set
{{(Sum V),(Sum I)},{(Sum V)}} is finite V42() set
the addF of a . [(Sum V),(Sum I)] is set
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() V133() associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of R is non empty set
a is Element of the carrier of R
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
the carrier of V is non empty set
<*> the carrier of V is Relation-like NAT -defined the carrier of V -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 V,K353( the carrier of V))
K353( the carrier of V) is functional non empty FinSequence-membered M12( the carrier of V)
Sum (<*> the carrier of V) is Element of the carrier of V
a * (Sum (<*> the carrier of V)) is Element of the carrier of V
0. V is V57(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
a * (0. V) is Element of the carrier of V
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() V133() associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of R is non empty set
a is Element of the carrier of R
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
the carrier of V is non empty set
v is Element of the carrier of V
u is Element of the carrier of V
<*v,u*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum <*v,u*> is Element of the carrier of V
a * (Sum <*v,u*>) is Element of the carrier of V
a * v is Element of the carrier of V
a * u is Element of the carrier of V
(a * v) + (a * u) is Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((a * v),(a * u)) is Element of the carrier of V
[(a * v),(a * u)] is set
{(a * v),(a * u)} is finite set
{(a * v)} is non empty trivial finite 1 -element set
{{(a * v),(a * u)},{(a * v)}} is finite V42() set
the addF of V . [(a * v),(a * u)] is set
v + u is Element of the carrier of V
the addF of V . (v,u) is Element of the carrier of V
[v,u] is set
{v,u} is finite set
{v} is non empty trivial finite 1 -element set
{{v,u},{v}} is finite V42() set
the addF of V . [v,u] is set
a * (v + u) is Element of the carrier of V
R is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() V133() associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of R is non empty set
a is Element of the carrier of R
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over R
the carrier of V is non empty set
v is Element of the carrier of V
u is Element of the carrier of V
w is Element of the carrier of V
<*v,u,w*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum <*v,u,w*> is Element of the carrier of V
a * (Sum <*v,u,w*>) is Element of the carrier of V
a * v is Element of the carrier of V
a * u is Element of the carrier of V
(a * v) + (a * u) is Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . ((a * v),(a * u)) is Element of the carrier of V
[(a * v),(a * u)] is set
{(a * v),(a * u)} is finite set
{(a * v)} is non empty trivial finite 1 -element set
{{(a * v),(a * u)},{(a * v)}} is finite V42() set
the addF of V . [(a * v),(a * u)] is set
a * w is Element of the carrier of V
((a * v) + (a * u)) + (a * w) is Element of the carrier of V
the addF of V . (((a * v) + (a * u)),(a * w)) is Element of the carrier of V
[((a * v) + (a * u)),(a * w)] is set
{((a * v) + (a * u)),(a * w)} is finite set
{((a * v) + (a * u))} is non empty trivial finite 1 -element set
{{((a * v) + (a * u)),(a * w)},{((a * v) + (a * u))}} is finite V42() set
the addF of V . [((a * v) + (a * u)),(a * w)] is set
v + u is Element of the carrier of V
the addF of V . (v,u) is Element of the carrier of V
[v,u] is set
{v,u} is finite set
{v} is non empty trivial finite 1 -element set
{{v,u},{v}} is finite V42() set
the addF of V . [v,u] is set
(v + u) + w is Element of the carrier of V
the addF of V . ((v + u),w) is Element of the carrier of V
[(v + u),w] is set
{(v + u),w} is finite set
{(v + u)} is non empty trivial finite 1 -element set
{{(v + u),w},{(v + u)}} is finite V42() set
the addF of V . [(v + u),w] is set
a * ((v + u) + w) is Element of the carrier of V
a * (v + u) is Element of the carrier of V
(a * (v + u)) + (a * w) is Element of the carrier of V
the addF of V . ((a * (v + u)),(a * w)) is Element of the carrier of V
[(a * (v + u)),(a * w)] is set
{(a * (v + u)),(a * w)} is finite set
{(a * (v + u))} is non empty trivial finite 1 -element set
{{(a * (v + u)),(a * w)},{(a * (v + u))}} is finite V42() set
the addF of V . [(a * (v + u)),(a * w)] is set