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

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

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

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

len v 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
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

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

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

K353( the carrier of R) is functional non empty FinSequence-membered M12( 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) + () is Element of the carrier of R
the addF of R . ((Sum I),()) is Element of the carrier of R
[(Sum I),()] is set
{(Sum I),()} is finite set
{(Sum I)} is non empty trivial finite 1 -element set
{{(Sum I),()},{(Sum I)}} is finite V42() set
the addF of R . [(Sum I),()] is set

Sum <*y*> is Element 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

Sum V is Element of the carrier of R
(Sum w) + () is Element of the carrier of R
the addF of R . ((Sum w),()) is Element of the carrier of R
[(Sum w),()] is set
{(Sum w),()} is finite set
{{(Sum w),()},{(Sum w)}} is finite V42() set
the addF of R . [(Sum w),()] is set

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

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

len v 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
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

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

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

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

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

the carrier of R is non empty set
a is ext-real V36() real Element of REAL

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

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

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

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

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

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

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

the carrier of R is non empty set

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

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

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

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

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

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)

dom I is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
I . (u + 1) is set

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

v1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT

v1 + v2 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT

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

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

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

dom q1 is finite V122() V123() V124() V125() V126() V127() Element of bool NAT

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

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

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

dom q2 is finite V122() V123() V124() V125() V126() V127() Element of bool NAT
v is Element of the carrier of R

K353( the carrier of R) is functional non empty FinSequence-membered M12( 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 + () 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

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

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

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

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

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

(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

(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

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

i is set

dom g is finite V122() V123() V124() V125() V126() V127() Element of bool (dom (q1 ^ q2))

j is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT

j1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT

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

j1 is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT

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

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

(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

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

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) + () is ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
((len q1) + ()) + 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

i 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)):]

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

(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

dom (<*v*> ^ q2) is finite V122() V123() V124() V125() V126() V127() Element of bool NAT

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

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

(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)) + () 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)),()) is Element of the carrier of R
[(Sum (q1 ^ q2)),()] is set
{(Sum (q1 ^ q2)),()} is finite set
{(Sum (q1 ^ q2))} is non empty trivial finite 1 -element set
{{(Sum (q1 ^ q2)),()},{(Sum (q1 ^ q2))}} is finite V42() set
the addF of R . [(Sum (q1 ^ q2)),()] 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)) + () 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) + (Sum q2))} is non empty trivial finite 1 -element set
{{((Sum q1) + (Sum q2)),()},{((Sum q1) + (Sum q2))}} is finite V42() set
the addF of R . [((Sum q1) + (Sum q2)),()] is set
() + (Sum q2) is Element of the carrier of R
the addF of R . ((),(Sum q2)) is Element of the carrier of R
[(),(Sum q2)] is set
{(),(Sum q2)} is finite set
{()} is non empty trivial finite 1 -element set
{{(),(Sum q2)},{()}} is finite V42() set
the addF of R . [(),(Sum q2)] is set
(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),(() + (Sum q2))},{(Sum q1)}} is finite V42() set
the addF of R . [(Sum q1),(() + (Sum q2))] is set

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

Sum (q1 ^ (<*v*> ^ q2)) is Element of the carrier of R
Sum w is Element 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

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

Sum w is Element of the carrier of R
Sum I is Element 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

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

the carrier of R is non empty set

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

Sum a is Element of the carrier of R
Sum V is Element of the carrier of R

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

a . (v . u) is set
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

rng V is finite set

Sum v is Element of the carrier of R
rng v is finite Element of bool 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

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

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

K353( the carrier of R) is functional non empty