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