:: RUSUB_3 semantic presentation

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

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() Element of bool REAL

bool REAL is non empty non trivial non finite set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() 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

the functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V40() cardinal {} -element FinSequence-membered V120() V121() V122() V123() V124() V125() V126() set is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V40() cardinal {} -element FinSequence-membered V120() V121() V122() V123() V124() V125() V126() 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

[:NAT,REAL:] is non empty non trivial non finite set

bool [:NAT,REAL:] 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

0 is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT

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

K64(0) is V25() set

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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 b

v is set

x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Sum x is Element of the carrier of V

ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination 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

r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Sum r3 is Element of the carrier of V

r4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Sum r4 is Element of the carrier of V

r3 + r4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

t is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

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

r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Sum r3 is Element of the carrier of V

u * r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

r4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Sum r4 is Element of the carrier of V

x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Sum x is Element of the carrier of V

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

W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of W2 is non empty set

v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of v is non empty set

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W2 is set

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

{ (Sum b

v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Sum v is Element of the carrier of V

{ (Sum b

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

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace 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

u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( 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

r2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

Carrier r2 is finite Element of bool the carrier of V

{ b

{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

r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {v}

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

{ b

r4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Sum r4 is Element of the carrier of V

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

(0). V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace 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

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

{} the carrier of V is functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V40() cardinal {} -element FinSequence-membered V120() V121() V122() V123() V124() V125() V126() Element of bool the carrier of V

bool the carrier of V is non empty set

(V,({} the carrier of V)) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(0). V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W2 is Element of the carrier of V

the carrier of (V,({} the carrier of V)) is non empty set

{ (Sum b

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

v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination 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

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

bool the carrier of V is non empty set

(0). V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

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

(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W2 is set

the Element of W1 is Element of W1

v is set

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

bool the carrier of V is non empty set

W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of W1 is non empty set

W2 is Element of bool the carrier of V

(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

v is Element of the carrier of V

x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2

Sum x is Element of the carrier of V

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR

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

(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(Omega). V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of ((Omega). V) is non empty set

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W1 /\ W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 /\ v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of V is non empty set

x is Element of the carrier of V

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 + v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W1 + W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace 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

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

v is Element of the carrier of V

x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Sum x is Element of the carrier of V

u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2

Sum u is Element of the carrier of V

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR

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

(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W2 is Element of bool the carrier of V

(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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,(W1 \/ W2)) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1) + (V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

v is Element of the carrier of V

x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1 \/ W2

Sum x is Element of the carrier of V

Carrier x is finite Element of bool the carrier of V

{ b

(Carrier x) \ W1 is finite Element of bool the carrier of V

(Carrier x) /\ 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

t is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)

a4 is Element of the carrier of V

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

a4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

Carrier a4 is finite Element of bool the carrier of V

{ b

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

a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)

b is Element of the carrier of V

a . b is ext-real V25() V26() Element of REAL

r6 is set

b is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

Carrier b is finite Element of bool the carrier of V

{ b

r6 is set

v is Element of the carrier of V

b . v is ext-real V25() V26() Element of REAL

a3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

r6 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2

a3 + r6 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

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

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

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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,(W1 /\ W2)) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1) /\ (V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

{ b

r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of r2

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

{ b

r4 is Relation-like Function-like set

dom r4 is set

rng r4 is set

t is non empty set

union t is set

the Relation-like t -defined union t -valued Function-like quasi_total Choice_Function of t is Relation-like t -defined union t -valued Function-like quasi_total Choice_Function of t

rng the Relation-like t -defined union t -valued Function-like quasi_total Choice_Function of t is set

a2 is set

r4 . a2 is set

a1 is set

a is Element of bool the carrier of V

{ b

dom the Relation-like t -defined union t -valued Function-like quasi_total Choice_Function of t is set

a2 is set

a1 is set

the Relation-like t -defined union t -valued Function-like quasi_total Choice_Function of t . a1 is set

a is set

r4 . a is set

{ b

b is Element of bool the carrier of V

a2 is set

a1 is set

union (rng the Relation-like t -defined union t -valued Function-like quasi_total Choice_Function of t) is set

a2 is Element of bool the carrier of V

a1 is set

r4 . a1 is set

{ b

the Relation-like t -defined union t -valued Function-like quasi_total Choice_Function of t . (r4 . a1) is set

b is Element of bool the carrier of V

r3 is Element of bool the carrier of V

(Omega). V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

v is set

x is Element of bool the carrier of V

(V,x) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace 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

r2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of x \/ {u}

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

{ b

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 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)

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

t is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

Carrier t is finite Element of bool the carrier of V

{ b

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 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)

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

a1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

Carrier a1 is finite Element of bool the carrier of V

{ b

a is set

b is Element of the carrier of V

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

a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {u}

Sum a is Element of the carrier of V

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

a4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of x

a4 - a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

- a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

(- 1) * a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

a4 + (- a) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination 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

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace 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

{ b

r2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of u

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

{ b

r3 is Relation-like Function-like set

dom r3 is set

rng r3 is set

r4 is non empty set

union r4 is set

the Relation-like r4 -defined union r4 -valued Function-like quasi_total Choice_Function of r4 is Relation-like r4 -defined union r4 -valued Function-like quasi_total Choice_Function of r4

rng the Relation-like r4 -defined union r4 -valued Function-like quasi_total Choice_Function of r4 is set

a3 is set

r3 . a3 is set

a2 is set

a1 is Element of bool the carrier of V

{ b

dom the Relation-like r4 -defined union r4 -valued Function-like quasi_total Choice_Function of r4 is set

a3 is set

a2 is set

the Relation-like r4 -defined union r4 -valued Function-like quasi_total Choice_Function of r4 . a2 is set

a1 is set

r3 . a1 is set

{ b

a is Element of bool the carrier of V

a3 is set

a2 is set

union (rng the Relation-like r4 -defined union r4 -valued Function-like quasi_total Choice_Function of r4) is set

a3 is Element of bool the carrier of V

a2 is set

r3 . a2 is set

{ b

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

{} the carrier of V is functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V40() cardinal {} -element FinSequence-membered V120() V121() V122() V123() V124() V125() V126() Element of bool the carrier of V

v is set

x is Element of bool the carrier of V

(V,x) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

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

r2 is Element of the carrier of V

r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Sum r3 is Element of the carrier of V

Carrier r3 is finite Element of bool the carrier of V

{ b

r4 is set

t is Element of the carrier of V

u is Element of bool the carrier of V

r4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of u

Sum r4 is Element of the carrier of V

(V,u) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace 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

r2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of x \/ {u}

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

{ b

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 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)

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

t is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

Carrier t is finite Element of bool the carrier of V

{ b

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 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)

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

a1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

Carrier a1 is finite Element of bool the carrier of V

{ b

a is set

b is Element of the carrier of V

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

a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {u}

Sum a is Element of the carrier of V

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

a4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of x

a4 - a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

- a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

(- 1) * a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

a4 + (- a) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination 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

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

{} the carrier of V is functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V40() cardinal {} -element FinSequence-membered V120() V121() V122() V123() V124() V125() V126() Element of bool the carrier of V

W1 is Element of bool the carrier of V

(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR

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,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

v is (V)

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W2 is Element of bool the carrier of V

(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

v is (V)

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

v is (V)

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

bool the carrier of V is non empty set

W1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

W2 is Element of bool the carrier of V

(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

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

v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng v is finite set

W1 (#) v 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 (#) v) is Element of the carrier of V

len v is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT

x is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT

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

u is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng u is finite set

len u is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT

W1 (#) u 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 (#) u) is Element of the carrier of V

r2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

r3 is set

<*r3*> is Relation-like NAT -defined Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set

r2 ^ <*r3*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

r4 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

r4 ^ <*r3*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like 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

a4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2

Sum a4 is Element of the carrier of V

a3 is Element of the carrier of V

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

r4 ^ <*a3*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence 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 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 <*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

W1 (#) r4 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) is Element of the carrier of V

a2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2

Sum a2 is Element of the carrier of V

W1 . a3 is ext-real V25() V26() Element of REAL

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

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

t is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

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

(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

x is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng x is finite set

len x is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT

W1 (#) x 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 (#) x) is Element of the carrier of V

<*> the carrier of V is Relation-like NAT -defined the carrier of V -valued Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V120() V121() V122() V123() V124() V125() V126() FinSequence 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

ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

Sum (ZeroLC V) is Element of the carrier of V

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

bool the carrier of V is non empty set

W1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

Carrier W1 is finite Element of bool the carrier of V

{ b

Sum W1 is Element of the carrier of V

W2 is Element of bool the carrier of V

(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

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

v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng v is finite set

W1 (#) v 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 (#) v) is Element of the carrier of V

x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2

Sum x is Element of the carrier of V

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

the carrier of W1 is non empty set

W2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

Carrier W2 is finite Element of bool the carrier of V

bool the carrier of V is non empty set

{ b

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

v is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Carrier v is finite Element of bool the carrier of W1

bool the carrier of W1 is non empty set

{ b

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

x is Relation-like NAT -defined the carrier of W1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of W1

rng x is finite set

v (#) x is Relation-like NAT -defined the carrier of W1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of W1

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

u is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng u is finite set

W2 (#) u is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

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

r2 is Relation-like dom x -defined dom x -valued Function-like one-to-one total quasi_total onto bijective finite Element of bool [:(dom x),(dom x):]

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

len (v (#) x) 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 x is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT

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

r3 is Relation-like NAT -defined the carrier of W1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of W1

len r3 is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT

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

t is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

len t is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT

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

a2 is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT

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

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

len u is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT

dom u is finite set

len (W2 (#) u) is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT

dom (W2 (#) u) is finite set

a2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal 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

card x is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT

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

r6 is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of 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

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

the carrier of W1 is non empty set

W2 is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Carrier W2 is finite Element of bool the carrier of W1

bool the carrier of W1 is non empty set

{ b

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 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

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

{ b

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

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

the carrier of W1 is non empty set

W2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

Carrier W2 is finite Element of bool the carrier of V

bool the carrier of V is non empty set

{ b

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

u is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Carrier u is finite Element of bool the carrier of W1

{ b

Sum u is Element of the carrier of W1

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W1 is (V)

(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of 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

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

bool the carrier of V is non empty set

W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

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

x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of v

Sum x is Element of the carrier of V

Carrier x is finite Element of bool the carrier of V

{ b

u is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Carrier u is finite Element of bool the carrier of W1

{ b

Sum u is Element of the carrier of W1

r2 is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of W2

Sum r2 is Element of the carrier of W1

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

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

bool the carrier of V is non empty set

W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

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

x is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of v

Sum x is Element of the carrier of W1

Carrier x is finite Element of bool the carrier of W1

{ b

u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

Carrier u is finite Element of bool the carrier of V

{ b

Sum u is Element of the carrier of V

r2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2

Sum r2 is Element of the carrier of V

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

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace 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)

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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,v) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

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

W1 \/ W1 is Element of bool the carrier of V

x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination 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

{ b

(V,{W2}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {W2}

Sum u is Element of the carrier of V

Carrier u is finite Element of bool the carrier of V

{ b

(Carrier x) \/ (Carrier u) is finite Element of bool the carrier of V

x - u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

- u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

(- 1) * u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

x + (- u) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V

Carrier (x - u) is finite Element of bool the carrier of V

{ b

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

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,r2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

bool the carrier of V is non empty set

W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

the carrier of W1 is non empty set

W2 is Element of bool the carrier of V

(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

v is set

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

x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2

Sum x is Element of the carrier of V

Carrier x is finite Element of bool the carrier of V

{ b

u is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of W1

Carrier u is finite Element of bool the carrier of W1

bool the carrier of W1 is non empty set

{ b