:: RUSUB_3 semantic presentation

REAL is non empty non trivial non finite V120() V121() V122() V126() set

bool REAL is non empty non trivial non finite set

bool NAT 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 V120() V126() set
RAT is non empty non trivial non finite V120() V121() V122() V123() V126() set
INT is non empty non trivial non finite V120() V121() V122() V123() V124() V126() set
{} is set

2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
is non empty non trivial non finite set
bool is non empty non trivial non finite set
1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
3 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
Seg 1 is non empty trivial finite 1 -element V120() V121() V122() V123() V124() V125() Element of bool NAT

- 1 is ext-real V25() V26() Element of REAL
K64(0) is V25() set

the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1 : verum } is set
v is set

Sum x is Element of the carrier of V

v is Element of bool the carrier of V
u is Element of the carrier of V
r2 is Element of the carrier of V
u + r2 is Element of the carrier of V

Sum r3 is Element of the carrier of V

Sum r4 is Element of the carrier of V

Sum t is Element of the carrier of V
u is ext-real V25() V26() Element of REAL
r2 is Element of the carrier of V
u * r2 is Element of the carrier of V

Sum r3 is Element of the carrier of V

Sum r4 is Element of the carrier of V

Sum x is Element of the carrier of V
0. V is V55(V) Element of the carrier of V

the carrier of W2 is non empty set

the carrier of v is non empty set

the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V

W2 is set
the carrier of (V,W1) is non empty set
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1 : verum } is set

Sum v is Element of the carrier of V
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1 : verum } is set
the carrier of (V,W1) is non empty set

the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V

W2 is set
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
v is Element of the carrier of V
x is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
x . v is ext-real V25() V26() Element of REAL
Funcs ( the carrier of V,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of V, REAL

{v} is non empty trivial finite 1 -element Element of bool the carrier of V
r2 is non empty trivial finite 1 -element Element of bool the carrier of V
r3 is Element of the carrier of V
u . r3 is ext-real V25() V26() Element of REAL
r3 is finite Element of bool the carrier of V

Carrier r2 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r2 . b1 = 0 } is set
{v} is non empty trivial finite 1 -element Element of bool the carrier of V
r3 is set
r4 is Element of the carrier of V
r2 . r4 is ext-real V25() V26() Element of REAL

Sum r3 is Element of the carrier of V
1 * v is Element of the carrier of V
Carrier r3 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r3 . b1 = 0 } is set

Sum r4 is Element of the carrier of V

0. V is V55(V) Element of the carrier of V
the carrier of V is non empty set
W1 is set
the carrier of ((0). V) is non empty set
{(0. V)} is non empty trivial finite 1 -element Element of bool the carrier of V
bool the carrier of V is non empty set

the carrier of V is non empty set

bool the carrier of V is non empty set

W2 is Element of the carrier of V
the carrier of (V,({} the carrier of V)) is non empty set
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {} the carrier of V : verum } is set
0. V is V55(V) Element of the carrier of V

Sum v is Element of the carrier of V
0. V is V55(V) Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set

0. V is V55(V) Element of the carrier of V
{(0. V)} is non empty trivial finite 1 -element Element of bool the carrier of V
W1 is Element of bool the carrier of V

W2 is set
the Element of W1 is Element of W1
v is set

the carrier of V is non empty set
bool the carrier of V is non empty set

the carrier of W1 is non empty set
W2 is Element of bool the carrier of V

v is Element of the carrier of V

Sum x is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V

the carrier of () is non empty set

the carrier of V is non empty set
x is Element of the carrier of V

the carrier of V is non empty set
x is Element of the carrier of V
u is Element of the carrier of V
r2 is Element of the carrier of V
u + r2 is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
W2 is Element of bool the carrier of V

v is Element of the carrier of V

Sum x is Element of the carrier of V

Sum u is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V

W2 is Element of bool the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
W2 is Element of bool the carrier of V
W1 \/ W2 is Element of bool the carrier of V

v is Element of the carrier of V

Sum x is Element of the carrier of V
Carrier x is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not x . b1 = 0 } is set
() \ W1 is finite Element of bool the carrier of V
() /\ W1 is finite Element of bool the carrier of V
r3 is set
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
r4 is Element of the carrier of V
t is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
t . r4 is ext-real V25() V26() Element of REAL
x . r3 is set
r3 is set
x . r3 is set
r3 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
Funcs ( the carrier of V,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of V, REAL
r4 is finite Element of bool the carrier of V

a4 is Element of the carrier of V
t . a4 is ext-real V25() V26() Element of REAL

Carrier a4 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not a4 . b1 = 0 } is set
a3 is set
a2 is Element of the carrier of V
a4 . a2 is ext-real V25() V26() Element of REAL
a2 is set
a1 is Element of the carrier of V
a is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
a . a1 is ext-real V25() V26() Element of REAL
x . a2 is set
a2 is set
x . a2 is set
a2 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
a1 is finite Element of bool the carrier of V

b is Element of the carrier of V
a . b is ext-real V25() V26() Element of REAL
r6 is set

Carrier b is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not b . b1 = 0 } is set
r6 is set
v is Element of the carrier of V
b . v is ext-real V25() V26() Element of REAL

v is Element of the carrier of V
x . v is ext-real V25() V26() Element of REAL
(a3 + r6) . v is ext-real V25() V26() Element of REAL
a3 . v is ext-real V25() V26() Element of REAL
r6 . v is ext-real V25() V26() Element of REAL
(a3 . v) + (r6 . v) is ext-real V25() V26() Element of REAL
(x . v) + (r6 . v) is ext-real V25() V26() Element of REAL
(x . v) + 0 is ext-real V25() V26() Element of REAL
a3 . v is ext-real V25() V26() Element of REAL
r6 . v is ext-real V25() V26() Element of REAL
(a3 . v) + (r6 . v) is ext-real V25() V26() Element of REAL
0 + (r6 . v) is ext-real V25() V26() Element of REAL
a3 . v is ext-real V25() V26() Element of REAL
r6 . v is ext-real V25() V26() Element of REAL
(a3 . v) + (r6 . v) is ext-real V25() V26() Element of REAL
0 + (r6 . v) is ext-real V25() V26() Element of REAL

Sum a3 is Element of the carrier of V
Sum r6 is Element of the carrier of V
(Sum a3) + (Sum r6) is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
W2 is Element of bool the carrier of V
W1 /\ W2 is Element of bool the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
the U5 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty non trivial non finite set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined REAL -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:],REAL:]
[:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) is non empty strict UNITSTR
W1 is Element of bool the carrier of V
W2 is set
v is set
the Element of v is Element of v
union v is set
r2 is set
r3 is set
r2 is Element of bool the carrier of V
{ b1 where b1 is Element of bool the carrier of V : ( a1 in b1 & b1 in v ) } is set

Sum r3 is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
Carrier r3 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r3 . b1 = 0 } is set

dom r4 is set
rng r4 is set
t is non empty set
union t is set

a2 is set
r4 . a2 is set
a1 is set
a is Element of bool the carrier of V
{ b1 where b1 is Element of bool the carrier of V : ( a2 in b1 & b1 in v ) } is set

a2 is set
a1 is set

a is set
r4 . a is set
{ b1 where b1 is Element of bool the carrier of V : ( a in b1 & b1 in v ) } is set
b is Element of bool the carrier of V
a2 is set
a1 is set
union () is set
a2 is Element of bool the carrier of V
a1 is set
r4 . a1 is set
{ b1 where b1 is Element of bool the carrier of V : ( a1 in b1 & b1 in v ) } is set

b is Element of bool the carrier of V
r3 is Element of bool the carrier of V

v is set
x is Element of bool the carrier of V

u is Element of the carrier of V
{u} is non empty trivial finite 1 -element Element of bool the carrier of V
x \/ {u} is Element of bool the carrier of V

Sum r2 is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
Carrier r2 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r2 . b1 = 0 } is set
r2 . u is ext-real V25() V26() Element of REAL
- (r2 . u) is ext-real V25() V26() Element of REAL
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
r3 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
r3 . u is ext-real V25() V26() Element of REAL
Funcs ( the carrier of V,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of V, REAL
t is Element of the carrier of V
(Carrier r2) \ {u} is finite Element of bool the carrier of V
r2 . t is ext-real V25() V26() Element of REAL

r4 . t is ext-real V25() V26() Element of REAL

Carrier t is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not t . b1 = 0 } is set
a4 is set
a3 is Element of the carrier of V
t . a3 is ext-real V25() V26() Element of REAL
r2 . a3 is ext-real V25() V26() Element of REAL
a3 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
a3 . u is ext-real V25() V26() Element of REAL
a1 is Element of the carrier of V

a2 . a1 is ext-real V25() V26() Element of REAL

Carrier a1 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not a1 . b1 = 0 } is set
a is set
b is Element of the carrier of V
a1 . b is ext-real V25() V26() Element of REAL

Sum a is Element of the carrier of V
(- (r2 . u)) * u is Element of the carrier of V

b is Element of the carrier of V
(a4 - a) . b is ext-real V25() V26() Element of REAL
r2 . b is ext-real V25() V26() Element of REAL
a4 . b is ext-real V25() V26() Element of REAL
a . b is ext-real V25() V26() Element of REAL
(a4 . b) - (a . b) is ext-real V25() V26() Element of REAL
a4 . b is ext-real V25() V26() Element of REAL
a . b is ext-real V25() V26() Element of REAL
(a4 . b) - (a . b) is ext-real V25() V26() Element of REAL
(r2 . b) - (a . b) is ext-real V25() V26() Element of REAL
(r2 . b) - 0 is ext-real V25() V26() Element of REAL
Sum a4 is Element of the carrier of V
(Sum a4) - (Sum a) is Element of the carrier of V
- (Sum a) is Element of the carrier of V
K194(V,(Sum a4),(- (Sum a))) is Element of the carrier of V
(0. V) + (Sum a) is Element of the carrier of V
(- (r2 . u)) " is ext-real V25() V26() Element of REAL
((- (r2 . u)) ") * ((- (r2 . u)) * u) is Element of the carrier of V
((- (r2 . u)) ") * (- (r2 . u)) is ext-real V25() V26() Element of REAL
(((- (r2 . u)) ") * (- (r2 . u))) * u is Element of the carrier of V
1 * u is Element of the carrier of V
r3 is set

the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V

W2 is set
v is set
union v is set
u is set
r2 is set
u is Element of bool the carrier of V
{ b1 where b1 is Element of bool the carrier of V : ( a1 in b1 & b1 in v ) } is set

Sum r2 is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
Carrier r2 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r2 . b1 = 0 } is set

dom r3 is set
rng r3 is set
r4 is non empty set
union r4 is set

a3 is set
r3 . a3 is set
a2 is set
a1 is Element of bool the carrier of V
{ b1 where b1 is Element of bool the carrier of V : ( a3 in b1 & b1 in v ) } is set

a3 is set
a2 is set

a1 is set
r3 . a1 is set
{ b1 where b1 is Element of bool the carrier of V : ( a1 in b1 & b1 in v ) } is set
a is Element of bool the carrier of V
a3 is set
a2 is set
union () is set
a3 is Element of bool the carrier of V
a2 is set
r3 . a2 is set
{ b1 where b1 is Element of bool the carrier of V : ( a2 in b1 & b1 in v ) } is set
the Relation-like r4 -defined union r4 -valued Function-like quasi_total Choice_Function of r4 . (r3 . a2) is set
a is Element of bool the carrier of V
r2 is set
r3 is set
r4 is Element of bool the carrier of V

v is set
x is Element of bool the carrier of V

the carrier of (V,x) is non empty set
r2 is Element of the carrier of V

Sum r3 is Element of the carrier of V
Carrier r3 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r3 . b1 = 0 } is set
r4 is set
t is Element of the carrier of V
u is Element of bool the carrier of V

Sum r4 is Element of the carrier of V

u is Element of the carrier of V
u is Element of the carrier of V
{u} is non empty trivial finite 1 -element Element of bool the carrier of V
x \/ {u} is Element of bool the carrier of V

Sum r2 is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
Carrier r2 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r2 . b1 = 0 } is set
r2 . u is ext-real V25() V26() Element of REAL
- (r2 . u) is ext-real V25() V26() Element of REAL
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
r3 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
r3 . u is ext-real V25() V26() Element of REAL
Funcs ( the carrier of V,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of V, REAL
t is Element of the carrier of V
(Carrier r2) \ {u} is finite Element of bool the carrier of V
r2 . t is ext-real V25() V26() Element of REAL

r4 . t is ext-real V25() V26() Element of REAL

Carrier t is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not t . b1 = 0 } is set
a4 is set
a3 is Element of the carrier of V
t . a3 is ext-real V25() V26() Element of REAL
r2 . a3 is ext-real V25() V26() Element of REAL
a3 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
a3 . u is ext-real V25() V26() Element of REAL
a1 is Element of the carrier of V

a2 . a1 is ext-real V25() V26() Element of REAL

Carrier a1 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not a1 . b1 = 0 } is set
a is set
b is Element of the carrier of V
a1 . b is ext-real V25() V26() Element of REAL

Sum a is Element of the carrier of V
(- (r2 . u)) * u is Element of the carrier of V

b is Element of the carrier of V
(a4 - a) . b is ext-real V25() V26() Element of REAL
r2 . b is ext-real V25() V26() Element of REAL
a4 . b is ext-real V25() V26() Element of REAL
a . b is ext-real V25() V26() Element of REAL
(a4 . b) - (a . b) is ext-real V25() V26() Element of REAL
a4 . b is ext-real V25() V26() Element of REAL
a . b is ext-real V25() V26() Element of REAL
(a4 . b) - (a . b) is ext-real V25() V26() Element of REAL
(r2 . b) - (a . b) is ext-real V25() V26() Element of REAL
(r2 . b) - 0 is ext-real V25() V26() Element of REAL
Sum a4 is Element of the carrier of V
(Sum a4) - (Sum a) is Element of the carrier of V
- (Sum a) is Element of the carrier of V
K194(V,(Sum a4),(- (Sum a))) is Element of the carrier of V
(0. V) + (Sum a) is Element of the carrier of V
(- (r2 . u)) " is ext-real V25() V26() Element of REAL
((- (r2 . u)) ") * ((- (r2 . u)) * u) is Element of the carrier of V
((- (r2 . u)) ") * (- (r2 . u)) is ext-real V25() V26() Element of REAL
(((- (r2 . u)) ") * (- (r2 . u))) * u is Element of the carrier of V
1 * u is Element of the carrier of V
r3 is set

the carrier of V is non empty set
bool the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
the U5 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty non trivial non finite set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined REAL -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:],REAL:]
[:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) is non empty strict UNITSTR

W1 is Element of bool the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
W2 is Element of bool the carrier of V

v is (V)

the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V

W2 is Element of bool the carrier of V

v is (V)

the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
the ZeroF of V is Element of the carrier of V
the U5 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty non trivial non finite set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined REAL -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:],REAL:]
[:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) is non empty strict UNITSTR
W2 is Element of bool the carrier of V

v is (V)

the carrier of V is non empty set
bool the carrier of V is non empty set

W2 is Element of bool the carrier of V

the carrier of (V,W2) is non empty set

rng v is finite set

Sum (W1 (#) v) is Element of the carrier of V

rng u is finite set

Sum (W1 (#) u) is Element of the carrier of V

r3 is set

rng (r4 ^ <*r3*>) is finite set
rng r4 is finite set
rng <*r3*> is finite set
(rng r4) \/ (rng <*r3*>) is finite set
{r3} is non empty trivial finite 1 -element set
(rng r4) \/ {r3} is finite set

Sum a4 is Element of the carrier of V
a3 is Element of the carrier of V

len (r4 ^ <*a3*>) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT

(len r4) + (len <*a3*>) is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
(len r4) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT

Sum (W1 (#) r4) is Element of the carrier of V

Sum a2 is Element of the carrier of V
W1 . a3 is ext-real V25() V26() Element of REAL

a2 + ((W1 . a3) * a4) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

(W1 (#) r4) ^ (W1 (#) t) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum ((W1 (#) r4) ^ (W1 (#) t)) is Element of the carrier of V
Sum (W1 (#) t) is Element of the carrier of V
(Sum a2) + (Sum (W1 (#) t)) is Element of the carrier of V
(W1 . a3) * a3 is Element of the carrier of V
<*((W1 . a3) * a3)*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum <*((W1 . a3) * a3)*> is Element of the carrier of V
(Sum a2) + (Sum <*((W1 . a3) * a3)*>) is Element of the carrier of V
(W1 . a3) * (Sum a4) is Element of the carrier of V
(Sum a2) + ((W1 . a3) * (Sum a4)) is Element of the carrier of V
Sum ((W1 . a3) * a4) is Element of the carrier of V
(Sum a2) + (Sum ((W1 . a3) * a4)) is Element of the carrier of V
Sum (a2 + ((W1 . a3) * a4)) is Element of the carrier of V

rng x is finite set

Sum (W1 (#) x) is Element of the carrier of V

[:NAT, the carrier of V:] is non empty non trivial non finite set
0. V is V55(V) Element of the carrier of V

Sum () is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set

Carrier W1 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not W1 . b1 = 0 } is set
Sum W1 is Element of the carrier of V
W2 is Element of bool the carrier of V

the carrier of (V,W2) is non empty set

rng v is finite set

Sum (W1 (#) v) is Element of the carrier of V

Sum x is Element of the carrier of V

the carrier of V is non empty set

the carrier of W1 is non empty set

Carrier W2 is finite Element of bool the carrier of V
bool the carrier of V is non empty set
{ b1 where b1 is Element of the carrier of V : not W2 . b1 = 0 } is set
W2 | the carrier of W1 is Relation-like the carrier of V -defined REAL -valued Function-like Element of bool [: the carrier of V,REAL:]
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
Sum W2 is Element of the carrier of V

Carrier v is finite Element of bool the carrier of W1
bool the carrier of W1 is non empty set
{ b1 where b1 is Element of the carrier of W1 : not v . b1 = 0 } is set
Sum v is Element of the carrier of W1
dom v is set
x is set
u is Element of the carrier of W1
v . u is ext-real V25() V26() Element of REAL
W2 . u is set

rng x is finite set

Sum (v (#) x) is Element of the carrier of W1

rng u is finite set

Sum (W2 (#) u) is Element of the carrier of V
r2 is set
r3 is Element of the carrier of V
W2 . r3 is ext-real V25() V26() Element of REAL
v . r3 is set
dom x is finite set
[:(dom x),(dom x):] is finite set
bool [:(dom x),(dom x):] is non empty finite V40() set

x * r2 is Relation-like dom x -defined the carrier of W1 -valued Function-like finite Element of bool [:(dom x), the carrier of W1:]
[:(dom x), the carrier of W1:] is set
bool [:(dom x), the carrier of W1:] is non empty set

dom (v (#) x) is finite set
(v (#) x) * r2 is Relation-like dom x -defined the carrier of W1 -valued Function-like finite Element of bool [:(dom x), the carrier of W1:]

dom r3 is finite set
rng r3 is finite set
[:NAT, the carrier of W1:] is non empty non trivial non finite set
bool [:NAT, the carrier of W1:] is non empty non trivial non finite set
Sum r3 is Element of the carrier of W1
0. W1 is V55(W1) Element of the carrier of W1
a4 is Relation-like NAT -defined the carrier of W1 -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of W1:]
a4 . (len r3) is Element of the carrier of W1
a4 . 0 is Element of the carrier of W1
dom a4 is set
rng a4 is set
[:NAT, the carrier of V:] is non empty non trivial non finite set
bool [:NAT, the carrier of V:] is non empty non trivial non finite set

a3 is Relation-like NAT -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of V:]

t . (a2 + 1) is set
a3 . (a2 + 1) is Element of the carrier of V
a3 . a2 is Element of the carrier of V
a1 is Element of the carrier of V
(a3 . a2) + a1 is Element of the carrier of V
a4 . (a2 + 1) is Element of the carrier of W1
a4 . a2 is Element of the carrier of W1
a is Element of the carrier of W1
(a4 . a2) + a is Element of the carrier of W1

dom u is finite set

dom (W2 (#) u) is finite set

u /. a2 is Element of the carrier of V
r2 . a2 is set
u . a2 is set
dom r2 is finite set
rng r2 is finite set

Seg (card x) is finite card x -element V120() V121() V122() V123() V124() V125() Element of bool NAT

x /. r6 is Element of the carrier of W1
x . (r2 . a2) is set
r3 . a2 is set
(v (#) x) . r6 is set
b is Element of the carrier of W1
v . b is ext-real V25() V26() Element of REAL
(v . b) * b is Element of the carrier of W1
W2 . (u /. a2) is ext-real V25() V26() Element of REAL
(W2 . (u /. a2)) * b is Element of the carrier of W1
(W2 . (u /. a2)) * (u /. a2) is Element of the carrier of V
(W2 (#) u) . a2 is set
[:(dom (v (#) x)),(dom (v (#) x)):] is finite set
bool [:(dom (v (#) x)),(dom (v (#) x)):] is non empty finite V40() set
a2 is Relation-like dom (v (#) x) -defined dom (v (#) x) -valued Function-like one-to-one total quasi_total onto bijective finite Element of bool [:(dom (v (#) x)),(dom (v (#) x)):]
(v (#) x) * a2 is Relation-like dom (v (#) x) -defined the carrier of W1 -valued Function-like finite Element of bool [:(dom (v (#) x)), the carrier of W1:]
[:(dom (v (#) x)), the carrier of W1:] is set
bool [:(dom (v (#) x)), the carrier of W1:] is non empty set
a3 . (len t) is Element of the carrier of V
a3 . 0 is Element of the carrier of V
0. V is V55(V) Element of the carrier of V

the carrier of V is non empty set

the carrier of W1 is non empty set

Carrier W2 is finite Element of bool the carrier of W1
bool the carrier of W1 is non empty set
{ b1 where b1 is Element of the carrier of W1 : not W2 . b1 = 0 } is set
Sum W2 is Element of the carrier of W1
[: the carrier of W1,REAL:] is non empty non trivial non finite set
bool [: the carrier of W1,REAL:] is non empty non trivial non finite set
bool the carrier of V is non empty set
u is set
W2 . u is set
r2 is Element of the carrier of V
r3 is Element of the carrier of W1
W2 . r3 is ext-real V25() V26() Element of REAL
W2 . r3 is set
r2 is Element of the carrier of V
r2 is Element of the carrier of V
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
u is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
u is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
r2 is Element of the carrier of V
x is finite Element of bool the carrier of V
W2 . r2 is set
u . r2 is ext-real V25() V26() Element of REAL
Funcs ( the carrier of V,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of V, REAL

r2 | the carrier of W1 is Relation-like the carrier of V -defined REAL -valued Function-like Element of bool [: the carrier of V,REAL:]
Carrier r2 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r2 . b1 = 0 } is set
Sum r2 is Element of the carrier of V
r4 is set
t is Element of the carrier of V
r2 . t is ext-real V25() V26() Element of REAL
r4 is set
r2 . r4 is set
W2 . r4 is set
v is Relation-like the carrier of W1 -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of W1,REAL:]
v . r4 is set
r3 is Relation-like the carrier of W1 -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of W1,REAL:]
r3 . r4 is set

the carrier of V is non empty set

the carrier of W1 is non empty set

Carrier W2 is finite Element of bool the carrier of V
bool the carrier of V is non empty set
{ b1 where b1 is Element of the carrier of V : not W2 . b1 = 0 } is set
Sum W2 is Element of the carrier of V
bool the carrier of W1 is non empty set
[: the carrier of W1,REAL:] is non empty non trivial non finite set
bool [: the carrier of W1,REAL:] is non empty non trivial non finite set
W2 | the carrier of W1 is Relation-like the carrier of V -defined REAL -valued Function-like Element of bool [: the carrier of V,REAL:]
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
x is Relation-like the carrier of W1 -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of W1,REAL:]
Funcs ( the carrier of W1,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of W1, REAL
dom x is set
u is Element of the carrier of W1
v is finite Element of bool the carrier of W1
W2 . u is set
x . u is ext-real V25() V26() Element of REAL

Carrier u is finite Element of bool the carrier of W1
{ b1 where b1 is Element of the carrier of W1 : not u . b1 = 0 } is set
Sum u is Element of the carrier of W1

the carrier of V is non empty set
W1 is (V)

W2 is Element of the carrier of V
the ZeroF of V is Element of the carrier of V
the U5 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty non trivial non finite set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined REAL -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:],REAL:]
[:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) is non empty strict UNITSTR

the carrier of V is non empty set
bool the carrier of V is non empty set

the carrier of W1 is non empty set
bool the carrier of W1 is non empty set
W2 is Element of bool the carrier of W1
v is Element of bool the carrier of V
0. V is V55(V) Element of the carrier of V

Sum x is Element of the carrier of V
Carrier x is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not x . b1 = 0 } is set

Carrier u is finite Element of bool the carrier of W1
{ b1 where b1 is Element of the carrier of W1 : not u . b1 = 0 } is set
Sum u is Element of the carrier of W1

Sum r2 is Element of the carrier of W1
0. W1 is V55(W1) Element of the carrier of W1

the carrier of V is non empty set
bool the carrier of V is non empty set

the carrier of W1 is non empty set
bool the carrier of W1 is non empty set
W2 is Element of bool the carrier of V
v is Element of bool the carrier of W1
0. W1 is V55(W1) Element of the carrier of W1

Sum x is Element of the carrier of W1
Carrier x is finite Element of bool the carrier of W1
{ b1 where b1 is Element of the carrier of W1 : not x . b1 = 0 } is set

Carrier u is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not u . b1 = 0 } is set
Sum u is Element of the carrier of V

Sum r2 is Element of the carrier of V
0. V is V55(V) Element of the carrier of V

W2 is (W1)
the carrier of V is non empty set
bool the carrier of V is non empty set
v is linearly-independent Element of bool the carrier of V
x is (V)

the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
W2 is Element of the carrier of V
{W2} is non empty trivial finite 1 -element Element of bool the carrier of V
W1 \ {W2} is Element of bool the carrier of V
bool W1 is non empty set
v is Element of bool the carrier of V

v \/ {W2} is Element of bool the carrier of V
W1 \/ W1 is Element of bool the carrier of V

Sum x is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
Carrier x is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not x . b1 = 0 } is set

Sum u is Element of the carrier of V
Carrier u is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not u . b1 = 0 } is set
() \/ () is finite Element of bool the carrier of V

Carrier (x - u) is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not (x - u) . b1 = 0 } is set
r2 is Element of the carrier of V
u . r2 is ext-real V25() V26() Element of REAL
r2 is set
r3 is Element of the carrier of V
x . r3 is ext-real V25() V26() Element of REAL
(x - u) . r3 is ext-real V25() V26() Element of REAL
u . r3 is ext-real V25() V26() Element of REAL
(x . r3) - (u . r3) is ext-real V25() V26() Element of REAL
(x . r3) - 0 is ext-real V25() V26() Element of REAL
- (Sum u) is Element of the carrier of V
(Sum x) + (- (Sum u)) is Element of the carrier of V
Sum (- u) is Element of the carrier of V
(Sum x) + (Sum (- u)) is Element of the carrier of V
Sum (x - u) is Element of the carrier of V
r2 is set
V is set
W1 is set
{W1} is non empty trivial finite 1 -element set
V \ {W1} is Element of bool V
bool V is non empty set
V /\ {W1} is finite set
W2 is set

the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is (V)
W2 is non empty Element of bool the carrier of V
W1 \/ W2 is Element of bool the carrier of V
v is set
x is Element of bool the carrier of V
u is Element of the carrier of V
{u} is non empty trivial finite 1 -element Element of bool the carrier of V
x \ {u} is Element of bool the carrier of V
W1 \ {u} is Element of bool the carrier of V
r2 is Element of bool the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set

the carrier of W1 is non empty set
W2 is Element of bool the carrier of V

v is set
the carrier of (V,W2) is non empty set

Sum x is Element of the carrier of V
Carrier x is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not x . b1 = 0 } is set

Carrier u is finite Element of bool the carrier of W1
bool the carrier of W1 is non empty set
{ b1 where b1 is Element of the carrier of W1 : not u . b1 =