:: RLVECT_4 semantic presentation

REAL is non empty V5() V26() set

NAT is non empty V17() V18() V19() Element of K32(REAL)

K32(REAL) is set

NAT is non empty V17() V18() V19() set

K32(NAT) is set

K32(NAT) is set

COMPLEX is non empty V5() V26() set

RAT is non empty V5() V26() set

INT is non empty V5() V26() set

2 is non empty V17() V18() V19() V23() V24() V25() V41() Element of NAT

{} is set

the empty V17() V18() V19() V21() V22() V23() V24() V25() V26() V30() V41() set is empty V17() V18() V19() V21() V22() V23() V24() V25() V26() V30() V41() set

1 is non empty V17() V18() V19() V23() V24() V25() V41() Element of NAT

0 is V17() V18() V19() V23() V24() V25() V41() Element of NAT

- 1 is V24() V25() V41() Element of REAL

K107(0) is V24() V25() V41() set

F

F

F

F

F

K33(F

K32(K33(F

F

F

F

V is Element of F

F

v is Element of F

w is Element of F

u is Element of F

V is V7() V10(F

V . F

V . F

V . F

v is Element of F

V . v is Element of F

F

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

{v} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

w is V24() V25() V41() Element of REAL

K33( the carrier of V,REAL) is set

K32(K33( the carrier of V,REAL)) is set

u is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of K32(K33( the carrier of V,REAL))

u . v is V24() V25() V41() Element of REAL

Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL

b is Element of the carrier of V

a is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of Funcs ( the carrier of V,REAL)

a . b is V24() V25() V41() Element of REAL

b is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of V

Carrier b is Element of K32( the carrier of V)

c is set

b . c is set

c is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of {v}

c . v is V24() V25() V41() Element of REAL

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

{v,w} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

u is V24() V25() V41() Element of REAL

a is V24() V25() V41() Element of REAL

K33( the carrier of V,REAL) is set

K32(K33( the carrier of V,REAL)) is set

b is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of K32(K33( the carrier of V,REAL))

b . v is V24() V25() V41() Element of REAL

b . w is V24() V25() V41() Element of REAL

Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL

r3 is Element of the carrier of V

c is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of Funcs ( the carrier of V,REAL)

c . r3 is V24() V25() V41() Element of REAL

r3 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of V

Carrier r3 is Element of K32( the carrier of V)

r4 is set

r3 . r4 is set

r4 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of {v,w}

r4 . v is V24() V25() V41() Element of REAL

r4 . w is V24() V25() V41() Element of REAL

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

u is Element of the carrier of V

{v,w,u} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

a is V24() V25() V41() Element of REAL

b is V24() V25() V41() Element of REAL

c is V24() V25() V41() Element of REAL

K33( the carrier of V,REAL) is set

K32(K33( the carrier of V,REAL)) is set

r3 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of K32(K33( the carrier of V,REAL))

r3 . v is V24() V25() V41() Element of REAL

r3 . w is V24() V25() V41() Element of REAL

r3 . u is V24() V25() V41() Element of REAL

Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL

t is Element of the carrier of V

r4 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of Funcs ( the carrier of V,REAL)

r4 . t is V24() V25() V41() Element of REAL

t is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of V

Carrier t is Element of K32( the carrier of V)

a4 is set

t . a4 is set

a4 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of {v,w,u}

a4 . v is V24() V25() V41() Element of REAL

a4 . w is V24() V25() V41() Element of REAL

a4 . u is V24() V25() V41() Element of REAL

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

v - v is Element of the carrier of V

- v is Element of the carrier of V

K196(V,v,(- v)) is Element of the carrier of V

w is Element of the carrier of V

v + w is Element of the carrier of V

(v + w) - v is Element of the carrier of V

K196(V,(v + w),(- v)) is Element of the carrier of V

w + v is Element of the carrier of V

(w + v) - v is Element of the carrier of V

K196(V,(w + v),(- v)) is Element of the carrier of V

(v - v) + w is Element of the carrier of V

w - v is Element of the carrier of V

K196(V,w,(- v)) is Element of the carrier of V

(w - v) + v is Element of the carrier of V

v + (w - v) is Element of the carrier of V

w + (v - v) is Element of the carrier of V

v - w is Element of the carrier of V

- w is Element of the carrier of V

K196(V,v,(- w)) is Element of the carrier of V

v - (v - w) is Element of the carrier of V

- (v - w) is Element of the carrier of V

K196(V,v,(- (v - w))) is Element of the carrier of V

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

(0. V) + w is Element of the carrier of V

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

v - w is Element of the carrier of V

- w is Element of the carrier of V

K196(V,v,(- w)) is Element of the carrier of V

u is Element of the carrier of V

u - w is Element of the carrier of V

K196(V,u,(- w)) is Element of the carrier of V

- (v - w) is Element of the carrier of V

w - u is Element of the carrier of V

- u is Element of the carrier of V

K196(V,w,(- u)) is Element of the carrier of V

w - v is Element of the carrier of V

- v is Element of the carrier of V

K196(V,w,(- v)) is Element of the carrier of V

V is V24() V25() V41() Element of REAL

- V is V24() V25() V41() Element of REAL

v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of v is non empty set

w is Element of the carrier of v

V * w is Element of the carrier of v

- (V * w) is Element of the carrier of v

(- V) * w is Element of the carrier of v

- w is Element of the carrier of v

V * (- w) is Element of the carrier of v

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V

v + w is Element of K32( the carrier of V)

K32( the carrier of V) is set

u is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V

v + u is Element of K32( the carrier of V)

a is set

b is Element of the carrier of V

v + b is Element of the carrier of V

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

u is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V

w + u is Element of K32( the carrier of V)

K32( the carrier of V) is set

v + u is Element of K32( the carrier of V)

a is Coset of u

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

u is Element of the carrier of V

{v,w,u} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

a is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of {v,w,u}

Sum a is Element of the carrier of V

a . v is V24() V25() V41() Element of REAL

(a . v) * v is Element of the carrier of V

a . w is V24() V25() V41() Element of REAL

(a . w) * w is Element of the carrier of V

((a . v) * v) + ((a . w) * w) is Element of the carrier of V

a . u is V24() V25() V41() Element of REAL

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

(((a . v) * v) + ((a . w) * w)) + ((a . u) * u) is Element of the carrier of V

Carrier a is Element of K32( the carrier of V)

r4 is Element of the carrier of V

a . r4 is V24() V25() V41() Element of REAL

the Element of Carrier a is Element of Carrier a

a . the Element of Carrier a is set

ZeroLC V is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of V

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

((a . v) * v) + (0. V) is Element of the carrier of V

(((a . v) * v) + ((a . w) * w)) + (0. V) is Element of the carrier of V

{u} is V26() Element of K32( the carrier of V)

r4 is set

a . r4 is set

<*u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

a (#) <*u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

<*((a . u) * u)*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

rng <*u*> is set

Sum <*((a . u) * u)*> is Element of the carrier of V

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

(0. V) + ((a . u) * u) is Element of the carrier of V

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

((0. V) + (0. V)) + ((a . u) * u) is Element of the carrier of V

((a . v) * v) + (0. V) is Element of the carrier of V

(((a . v) * v) + (0. V)) + ((a . u) * u) is Element of the carrier of V

{w} is V26() Element of K32( the carrier of V)

r4 is set

a . r4 is set

<*w*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

a (#) <*w*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

<*((a . w) * w)*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

rng <*w*> is set

Sum <*((a . w) * w)*> is Element of the carrier of V

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

(0. V) + ((a . w) * w) is Element of the carrier of V

((0. V) + ((a . w) * w)) + (0. V) is Element of the carrier of V

(((a . v) * v) + ((a . w) * w)) + (0. V) is Element of the carrier of V

{w,u} is V26() Element of K32( the carrier of V)

r4 is set

a . r4 is set

<*w,u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

a (#) <*w,u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

<*((a . w) * w),((a . u) * u)*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

rng <*w,u*> is set

Sum <*((a . w) * w),((a . u) * u)*> is Element of the carrier of V

((a . w) * w) + ((a . u) * u) is Element of the carrier of V

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

(0. V) + ((a . w) * w) is Element of the carrier of V

((0. V) + ((a . w) * w)) + ((a . u) * u) is Element of the carrier of V

{v} is V26() Element of K32( the carrier of V)

r4 is set

a . r4 is set

<*v*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

a (#) <*v*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

<*((a . v) * v)*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

rng <*v*> is set

Sum <*((a . v) * v)*> is Element of the carrier of V

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

((a . v) * v) + (0. V) is Element of the carrier of V

(((a . v) * v) + (0. V)) + (0. V) is Element of the carrier of V

(((a . v) * v) + ((a . w) * w)) + (0. V) is Element of the carrier of V

{v,u} is V26() Element of K32( the carrier of V)

r4 is set

a . r4 is set

<*v,u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

a (#) <*v,u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

<*((a . v) * v),((a . u) * u)*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

rng <*v,u*> is set

Sum <*((a . v) * v),((a . u) * u)*> is Element of the carrier of V

((a . v) * v) + ((a . u) * u) is Element of the carrier of V

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

((a . v) * v) + (0. V) is Element of the carrier of V

(((a . v) * v) + (0. V)) + ((a . u) * u) is Element of the carrier of V

{v,w} is V26() Element of K32( the carrier of V)

r4 is set

a . r4 is set

<*v,w*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

a (#) <*v,w*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

<*((a . v) * v),((a . w) * w)*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

rng <*v,w*> is set

Sum <*((a . v) * v),((a . w) * w)*> is Element of the carrier of V

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

(((a . v) * v) + ((a . w) * w)) + (0. V) is Element of the carrier of V

r4 is set

<*v,w,u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

a (#) <*v,w,u*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

<*((a . v) * v),((a . w) * w),((a . u) * u)*> is V7() V10( NAT ) V11( the carrier of V) Function-like FinSequence-like FinSequence of the carrier of V

rng <*v,w,u*> is set

Sum <*((a . v) * v),((a . w) * w),((a . u) * u)*> is Element of the carrier of V

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

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

v is Element of the carrier of V

w is Element of the carrier of V

u is Element of the carrier of V

{v,w,u} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

a is V24() V25() V41() Element of REAL

a * v is Element of the carrier of V

b is V24() V25() V41() Element of REAL

b * w is Element of the carrier of V

(a * v) + (b * w) is Element of the carrier of V

c is V24() V25() V41() Element of REAL

c * u is Element of the carrier of V

((a * v) + (b * w)) + (c * u) is Element of the carrier of V

K33( the carrier of V,REAL) is set

K32(K33( the carrier of V,REAL)) is set

r3 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of K32(K33( the carrier of V,REAL))

r3 . v is V24() V25() V41() Element of REAL

r3 . w is V24() V25() V41() Element of REAL

r3 . u is V24() V25() V41() Element of REAL

Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL

t is Element of the carrier of V

r4 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Element of Funcs ( the carrier of V,REAL)

r4 . t is V24() V25() V41() Element of REAL

t is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of V

Carrier t is Element of K32( the carrier of V)

a4 is set

t . a4 is set

a4 is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of {v,w,u}

Sum a4 is Element of the carrier of V

Carrier a4 is Element of K32( the carrier of V)

1 * v is Element of the carrier of V

(- 1) * w is Element of the carrier of V

(1 * v) + ((- 1) * w) is Element of the carrier of V

0 * u is Element of the carrier of V

((1 * v) + ((- 1) * w)) + (0 * u) is Element of the carrier of V

(- 1) * v is Element of the carrier of V

v + ((- 1) * v) is Element of the carrier of V

(v + ((- 1) * v)) + (0 * u) is Element of the carrier of V

- v is Element of the carrier of V

v + (- v) is Element of the carrier of V

(v + (- v)) + (0 * u) is Element of the carrier of V

(v + (- v)) + (0. V) is Element of the carrier of V

1 * v is Element of the carrier of V

0 * w is Element of the carrier of V

(1 * v) + (0 * w) is Element of the carrier of V

(- 1) * u is Element of the carrier of V

((1 * v) + (0 * w)) + ((- 1) * u) is Element of the carrier of V

v + (0 * w) is Element of the carrier of V

(- 1) * v is Element of the carrier of V

(v + (0 * w)) + ((- 1) * v) is Element of the carrier of V

v + (0. V) is Element of the carrier of V

(v + (0. V)) + ((- 1) * v) is Element of the carrier of V

- v is Element of the carrier of V

(v + (0. V)) + (- v) is Element of the carrier of V

v + (- v) is Element of the carrier of V

0 * v is Element of the carrier of V

1 * w is Element of the carrier of V

(0 * v) + (1 * w) is Element of the carrier of V

(- 1) * u is Element of the carrier of V

((0 * v) + (1 * w)) + ((- 1) * u) is Element of the carrier of V

- w is Element of the carrier of V

((0 * v) + (1 * w)) + (- w) is Element of the carrier of V

(0. V) + (1 * w) is Element of the carrier of V

((0. V) + (1 * w)) + (- w) is Element of the carrier of V

(0. V) + w is Element of the carrier of V

((0. V) + w) + (- w) is Element of the carrier of V

w + (- w) is Element of the carrier of V

a is V7() V10( the carrier of V) V11( REAL ) Function-like quasi_total Linear_Combination of {v,w,u}

Sum a is Element of the carrier of V

Carrier a is Element of K32( the carrier of V)

a . v is V24() V25() V41() Element of REAL

(a . v) * v is Element of the carrier of V

a . w is V24() V25() V41() Element of REAL

(a . w) * w is Element of the carrier of V

((a . v) * v) + ((a . w) * w) is Element of the carrier of V

a . u is V24() V25() V41() Element of REAL

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

(((a . v) * v) + ((a . w) * w)) + ((a . u) * u) is Element of the carrier of V

b is set

V is set

v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of v is non empty set

w is Element of the carrier of v

{w} is V26() Element of K32( the carrier of v)

K32( the carrier of v) is set

Lin {w} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of v

u is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of {w}

Sum u is Element of the carrier of v

u . w is V24() V25() V41() Element of REAL

(u . w) * w is Element of the carrier of v

u is V24() V25() V41() Element of REAL

u * w is Element of the carrier of v

K33( the carrier of v,REAL) is set

K32(K33( the carrier of v,REAL)) is set

a is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Element of K32(K33( the carrier of v,REAL))

a . w is V24() V25() V41() Element of REAL

Funcs ( the carrier of v,REAL) is non empty FUNCTION_DOMAIN of the carrier of v, REAL

c is Element of the carrier of v

b is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Element of Funcs ( the carrier of v,REAL)

b . c is V24() V25() V41() Element of REAL

c is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of v

Carrier c is Element of K32( the carrier of v)

r3 is set

c . r3 is set

r3 is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of {w}

Sum r3 is Element of the carrier of v

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

{v} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

Lin {v} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V

V is set

v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of v is non empty set

w is Element of the carrier of v

u is Element of the carrier of v

{u} is V26() Element of K32( the carrier of v)

K32( the carrier of v) is set

Lin {u} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of v

w + (Lin {u}) is Element of K32( the carrier of v)

a is Element of the carrier of v

w + a is Element of the carrier of v

b is V24() V25() V41() Element of REAL

b * u is Element of the carrier of v

a is V24() V25() V41() Element of REAL

a * u is Element of the carrier of v

w + (a * u) is Element of the carrier of v

V is set

v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of v is non empty set

w is Element of the carrier of v

u is Element of the carrier of v

{w,u} is V26() Element of K32( the carrier of v)

K32( the carrier of v) is set

Lin {w,u} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of v

{w} is V26() Element of K32( the carrier of v)

a is V24() V25() V41() Element of REAL

a * w is Element of the carrier of v

0. v is V52(v) Element of the carrier of v

(a * w) + (0. v) is Element of the carrier of v

0 * u is Element of the carrier of v

(a * w) + (0 * u) is Element of the carrier of v

a is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of {w,u}

Sum a is Element of the carrier of v

a . w is V24() V25() V41() Element of REAL

(a . w) * w is Element of the carrier of v

a . u is V24() V25() V41() Element of REAL

(a . u) * u is Element of the carrier of v

((a . w) * w) + ((a . u) * u) is Element of the carrier of v

a is V24() V25() V41() Element of REAL

a * w is Element of the carrier of v

b is V24() V25() V41() Element of REAL

b * u is Element of the carrier of v

(a * w) + (b * u) is Element of the carrier of v

a is V24() V25() V41() Element of REAL

a * w is Element of the carrier of v

b is V24() V25() V41() Element of REAL

b * u is Element of the carrier of v

(a * w) + (b * u) is Element of the carrier of v

a + b is V24() V25() V41() Element of REAL

(a + b) * w is Element of the carrier of v

{w} is V26() Element of K32( the carrier of v)

Lin {w} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of v

K33( the carrier of v,REAL) is set

K32(K33( the carrier of v,REAL)) is set

c is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Element of K32(K33( the carrier of v,REAL))

c . w is V24() V25() V41() Element of REAL

c . u is V24() V25() V41() Element of REAL

Funcs ( the carrier of v,REAL) is non empty FUNCTION_DOMAIN of the carrier of v, REAL

r4 is Element of the carrier of v

r3 is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Element of Funcs ( the carrier of v,REAL)

r3 . r4 is V24() V25() V41() Element of REAL

r4 is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of v

Carrier r4 is Element of K32( the carrier of v)

t is set

r4 . t is set

t is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of {w,u}

Sum t is Element of the carrier of v

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

{v,w} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

Lin {v,w} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V

V is set

v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of v is non empty set

w is Element of the carrier of v

u is Element of the carrier of v

a is Element of the carrier of v

{u,a} is V26() Element of K32( the carrier of v)

K32( the carrier of v) is set

Lin {u,a} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of v

w + (Lin {u,a}) is Element of K32( the carrier of v)

b is Element of the carrier of v

w + b is Element of the carrier of v

c is V24() V25() V41() Element of REAL

c * u is Element of the carrier of v

r3 is V24() V25() V41() Element of REAL

r3 * a is Element of the carrier of v

(c * u) + (r3 * a) is Element of the carrier of v

w + (c * u) is Element of the carrier of v

(w + (c * u)) + (r3 * a) is Element of the carrier of v

b is V24() V25() V41() Element of REAL

b * u is Element of the carrier of v

w + (b * u) is Element of the carrier of v

c is V24() V25() V41() Element of REAL

c * a is Element of the carrier of v

(w + (b * u)) + (c * a) is Element of the carrier of v

(b * u) + (c * a) is Element of the carrier of v

w + ((b * u) + (c * a)) is Element of the carrier of v

V is set

v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of v is non empty set

w is Element of the carrier of v

u is Element of the carrier of v

a is Element of the carrier of v

{w,u,a} is V26() Element of K32( the carrier of v)

K32( the carrier of v) is set

Lin {w,u,a} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of v

b is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of {w,u,a}

Sum b is Element of the carrier of v

b . w is V24() V25() V41() Element of REAL

(b . w) * w is Element of the carrier of v

b . u is V24() V25() V41() Element of REAL

(b . u) * u is Element of the carrier of v

((b . w) * w) + ((b . u) * u) is Element of the carrier of v

b . a is V24() V25() V41() Element of REAL

(b . a) * a is Element of the carrier of v

(((b . w) * w) + ((b . u) * u)) + ((b . a) * a) is Element of the carrier of v

{w,a} is V26() Element of K32( the carrier of v)

{w,w,u} is V26() Element of K32( the carrier of v)

{a,a,w} is V26() Element of K32( the carrier of v)

{w,u} is V26() Element of K32( the carrier of v)

b is V24() V25() V41() Element of REAL

b * w is Element of the carrier of v

c is V24() V25() V41() Element of REAL

c * u is Element of the carrier of v

(b * w) + (c * u) is Element of the carrier of v

0. v is V52(v) Element of the carrier of v

((b * w) + (c * u)) + (0. v) is Element of the carrier of v

0 * a is Element of the carrier of v

((b * w) + (c * u)) + (0 * a) is Element of the carrier of v

b is V24() V25() V41() Element of REAL

b * w is Element of the carrier of v

c is V24() V25() V41() Element of REAL

c * a is Element of the carrier of v

(b * w) + (c * a) is Element of the carrier of v

0. v is V52(v) Element of the carrier of v

(b * w) + (0. v) is Element of the carrier of v

((b * w) + (0. v)) + (c * a) is Element of the carrier of v

0 * u is Element of the carrier of v

(b * w) + (0 * u) is Element of the carrier of v

((b * w) + (0 * u)) + (c * a) is Element of the carrier of v

{w,u} is V26() Element of K32( the carrier of v)

b is V24() V25() V41() Element of REAL

b * w is Element of the carrier of v

c is V24() V25() V41() Element of REAL

c * u is Element of the carrier of v

(b * w) + (c * u) is Element of the carrier of v

r3 is V24() V25() V41() Element of REAL

r3 * a is Element of the carrier of v

((b * w) + (c * u)) + (r3 * a) is Element of the carrier of v

b is V24() V25() V41() Element of REAL

b * w is Element of the carrier of v

c is V24() V25() V41() Element of REAL

c * u is Element of the carrier of v

(b * w) + (c * u) is Element of the carrier of v

r3 is V24() V25() V41() Element of REAL

r3 * a is Element of the carrier of v

((b * w) + (c * u)) + (r3 * a) is Element of the carrier of v

b is V24() V25() V41() Element of REAL

b * w is Element of the carrier of v

c is V24() V25() V41() Element of REAL

c * u is Element of the carrier of v

(b * w) + (c * u) is Element of the carrier of v

r3 is V24() V25() V41() Element of REAL

r3 * a is Element of the carrier of v

((b * w) + (c * u)) + (r3 * a) is Element of the carrier of v

{w,a} is V26() Element of K32( the carrier of v)

b + c is V24() V25() V41() Element of REAL

(b + c) * w is Element of the carrier of v

((b + c) * w) + (r3 * a) is Element of the carrier of v

{w,w,u} is V26() Element of K32( the carrier of v)

{u,w} is V26() Element of K32( the carrier of v)

r3 * w is Element of the carrier of v

(b * w) + (r3 * w) is Element of the carrier of v

(c * u) + ((b * w) + (r3 * w)) is Element of the carrier of v

b + r3 is V24() V25() V41() Element of REAL

(b + r3) * w is Element of the carrier of v

(c * u) + ((b + r3) * w) is Element of the carrier of v

{u,u,w} is V26() Element of K32( the carrier of v)

{w,u} is V26() Element of K32( the carrier of v)

r3 * u is Element of the carrier of v

(c * u) + (r3 * u) is Element of the carrier of v

(b * w) + ((c * u) + (r3 * u)) is Element of the carrier of v

c + r3 is V24() V25() V41() Element of REAL

(c + r3) * u is Element of the carrier of v

(b * w) + ((c + r3) * u) is Element of the carrier of v

K33( the carrier of v,REAL) is set

K32(K33( the carrier of v,REAL)) is set

r4 is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Element of K32(K33( the carrier of v,REAL))

r4 . w is V24() V25() V41() Element of REAL

r4 . u is V24() V25() V41() Element of REAL

r4 . a is V24() V25() V41() Element of REAL

Funcs ( the carrier of v,REAL) is non empty FUNCTION_DOMAIN of the carrier of v, REAL

a4 is Element of the carrier of v

t is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Element of Funcs ( the carrier of v,REAL)

t . a4 is V24() V25() V41() Element of REAL

a4 is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of v

Carrier a4 is Element of K32( the carrier of v)

a3 is set

a4 . a3 is set

a3 is V7() V10( the carrier of v) V11( REAL ) Function-like quasi_total Linear_Combination of {w,u,a}

Sum a3 is Element of the carrier of v

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

u is Element of the carrier of V

{v,w,u} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

Lin {v,w,u} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V

V is set

v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of v is non empty set

w is Element of the carrier of v

u is Element of the carrier of v

a is Element of the carrier of v

b is Element of the carrier of v

{u,a,b} is V26() Element of K32( the carrier of v)

K32( the carrier of v) is set

Lin {u,a,b} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of v

w + (Lin {u,a,b}) is Element of K32( the carrier of v)

c is Element of the carrier of v

w + c is Element of the carrier of v

r3 is V24() V25() V41() Element of REAL

r3 * u is Element of the carrier of v

r4 is V24() V25() V41() Element of REAL

r4 * a is Element of the carrier of v

(r3 * u) + (r4 * a) is Element of the carrier of v

t is V24() V25() V41() Element of REAL

t * b is Element of the carrier of v

((r3 * u) + (r4 * a)) + (t * b) is Element of the carrier of v

w + (r3 * u) is Element of the carrier of v

(w + (r3 * u)) + (r4 * a) is Element of the carrier of v

((w + (r3 * u)) + (r4 * a)) + (t * b) is Element of the carrier of v

w + ((r3 * u) + (r4 * a)) is Element of the carrier of v

(w + ((r3 * u) + (r4 * a))) + (t * b) is Element of the carrier of v

c is V24() V25() V41() Element of REAL

c * u is Element of the carrier of v

w + (c * u) is Element of the carrier of v

r3 is V24() V25() V41() Element of REAL

r3 * a is Element of the carrier of v

(w + (c * u)) + (r3 * a) is Element of the carrier of v

r4 is V24() V25() V41() Element of REAL

r4 * b is Element of the carrier of v

((w + (c * u)) + (r3 * a)) + (r4 * b) is Element of the carrier of v

(c * u) + (r3 * a) is Element of the carrier of v

((c * u) + (r3 * a)) + (r4 * b) is Element of the carrier of v

w + (((c * u) + (r3 * a)) + (r4 * b)) is Element of the carrier of v

w + ((c * u) + (r3 * a)) is Element of the carrier of v

(w + ((c * u) + (r3 * a))) + (r4 * b) is Element of the carrier of v

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

{v,w} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

w - v is Element of the carrier of V

- v is Element of the carrier of V

K196(V,w,(- v)) is Element of the carrier of V

{v,(w - v)} is V26() Element of K32( the carrier of V)

u is V24() V25() V41() Element of REAL

u * v is Element of the carrier of V

a is V24() V25() V41() Element of REAL

a * (w - v) is Element of the carrier of V

(u * v) + (a * (w - v)) is Element of the carrier of V

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

a * w is Element of the carrier of V

a * v is Element of the carrier of V

(a * w) - (a * v) is Element of the carrier of V

- (a * v) is Element of the carrier of V

K196(V,(a * w),(- (a * v))) is Element of the carrier of V

(u * v) + ((a * w) - (a * v)) is Element of the carrier of V

(u * v) + (a * w) is Element of the carrier of V

((u * v) + (a * w)) - (a * v) is Element of the carrier of V

K196(V,((u * v) + (a * w)),(- (a * v))) is Element of the carrier of V

(u * v) - (a * v) is Element of the carrier of V

K196(V,(u * v),(- (a * v))) is Element of the carrier of V

((u * v) - (a * v)) + (a * w) is Element of the carrier of V

u - a is V24() V25() V41() Element of REAL

(u - a) * v is Element of the carrier of V

((u - a) * v) + (a * w) is Element of the carrier of V

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

{v,w} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

w + v is Element of the carrier of V

{v,(w + v)} is V26() Element of K32( the carrier of V)

u is V24() V25() V41() Element of REAL

u * v is Element of the carrier of V

a is V24() V25() V41() Element of REAL

a * (w + v) is Element of the carrier of V

(u * v) + (a * (w + v)) is Element of the carrier of V

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

a * v is Element of the carrier of V

a * w is Element of the carrier of V

(a * v) + (a * w) is Element of the carrier of V

(u * v) + ((a * v) + (a * w)) is Element of the carrier of V

(u * v) + (a * v) is Element of the carrier of V

((u * v) + (a * v)) + (a * w) is Element of the carrier of V

u + a is V24() V25() V41() Element of REAL

(u + a) * v is Element of the carrier of V

((u + a) * v) + (a * w) is Element of the carrier of V

V is V24() V25() V41() Element of REAL

v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of v is non empty set

w is Element of the carrier of v

u is Element of the carrier of v

{w,u} is V26() Element of K32( the carrier of v)

K32( the carrier of v) is set

V * u is Element of the carrier of v

{w,(V * u)} is V26() Element of K32( the carrier of v)

a is V24() V25() V41() Element of REAL

a * w is Element of the carrier of v

b is V24() V25() V41() Element of REAL

b * (V * u) is Element of the carrier of v

(a * w) + (b * (V * u)) is Element of the carrier of v

0. v is V52(v) Element of the carrier of v

b * V is V24() V25() V41() Element of REAL

(b * V) * u is Element of the carrier of v

(a * w) + ((b * V) * u) is Element of the carrier of v

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

{v,w} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

- w is Element of the carrier of V

{v,(- w)} is V26() Element of K32( the carrier of V)

(- 1) * w is Element of the carrier of V

V is V24() V25() V41() Element of REAL

v is V24() V25() V41() Element of REAL

w is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of w is non empty set

u is Element of the carrier of w

V * u is Element of the carrier of w

v * u is Element of the carrier of w

{(V * u),(v * u)} is V26() Element of K32( the carrier of w)

K32( the carrier of w) is set

0. w is V52(w) Element of the carrier of w

0. w is V52(w) Element of the carrier of w

v * (V * u) is Element of the carrier of w

- V is V24() V25() V41() Element of REAL

(- V) * (v * u) is Element of the carrier of w

(v * (V * u)) + ((- V) * (v * u)) is Element of the carrier of w

V * v is V24() V25() V41() Element of REAL

(V * v) * u is Element of the carrier of w

((V * v) * u) + ((- V) * (v * u)) is Element of the carrier of w

V * (v * u) is Element of the carrier of w

((V * v) * u) - (V * (v * u)) is Element of the carrier of w

- (V * (v * u)) is Element of the carrier of w

K196(w,((V * v) * u),(- (V * (v * u)))) is Element of the carrier of w

((V * v) * u) - ((V * v) * u) is Element of the carrier of w

- ((V * v) * u) is Element of the carrier of w

K196(w,((V * v) * u),(- ((V * v) * u))) is Element of the carrier of w

0. w is V52(w) Element of the carrier of w

V is V24() V25() V41() Element of REAL

v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of v is non empty set

w is Element of the carrier of v

V * w is Element of the carrier of v

{w,(V * w)} is V26() Element of K32( the carrier of v)

K32( the carrier of v) is set

1 * w is Element of the carrier of v

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

u is Element of the carrier of V

{v,w,u} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

u - v is Element of the carrier of V

- v is Element of the carrier of V

K196(V,u,(- v)) is Element of the carrier of V

{v,w,(u - v)} is V26() Element of K32( the carrier of V)

a is V24() V25() V41() Element of REAL

a * v is Element of the carrier of V

b is V24() V25() V41() Element of REAL

b * w is Element of the carrier of V

(a * v) + (b * w) is Element of the carrier of V

c is V24() V25() V41() Element of REAL

c * (u - v) is Element of the carrier of V

((a * v) + (b * w)) + (c * (u - v)) is Element of the carrier of V

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

c * u is Element of the carrier of V

c * v is Element of the carrier of V

(c * u) - (c * v) is Element of the carrier of V

- (c * v) is Element of the carrier of V

K196(V,(c * u),(- (c * v))) is Element of the carrier of V

((a * v) + (b * w)) + ((c * u) - (c * v)) is Element of the carrier of V

(b * w) + ((c * u) - (c * v)) is Element of the carrier of V

(a * v) + ((b * w) + ((c * u) - (c * v))) is Element of the carrier of V

(b * w) + (c * u) is Element of the carrier of V

((b * w) + (c * u)) - (c * v) is Element of the carrier of V

K196(V,((b * w) + (c * u)),(- (c * v))) is Element of the carrier of V

(a * v) + (((b * w) + (c * u)) - (c * v)) is Element of the carrier of V

(b * w) - (c * v) is Element of the carrier of V

K196(V,(b * w),(- (c * v))) is Element of the carrier of V

((b * w) - (c * v)) + (c * u) is Element of the carrier of V

(a * v) + (((b * w) - (c * v)) + (c * u)) is Element of the carrier of V

(a * v) + ((b * w) - (c * v)) is Element of the carrier of V

((a * v) + ((b * w) - (c * v))) + (c * u) is Element of the carrier of V

((a * v) + (b * w)) - (c * v) is Element of the carrier of V

K196(V,((a * v) + (b * w)),(- (c * v))) is Element of the carrier of V

(((a * v) + (b * w)) - (c * v)) + (c * u) is Element of the carrier of V

(a * v) - (c * v) is Element of the carrier of V

K196(V,(a * v),(- (c * v))) is Element of the carrier of V

((a * v) - (c * v)) + (b * w) is Element of the carrier of V

(((a * v) - (c * v)) + (b * w)) + (c * u) is Element of the carrier of V

a - c is V24() V25() V41() Element of REAL

(a - c) * v is Element of the carrier of V

((a - c) * v) + (b * w) is Element of the carrier of V

(((a - c) * v) + (b * w)) + (c * u) is Element of the carrier of V

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

w - v is Element of the carrier of V

- v is Element of the carrier of V

K196(V,w,(- v)) is Element of the carrier of V

u is Element of the carrier of V

{v,w,u} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

u - v is Element of the carrier of V

K196(V,u,(- v)) is Element of the carrier of V

{v,(w - v),(u - v)} is V26() Element of K32( the carrier of V)

a is V24() V25() V41() Element of REAL

a * v is Element of the carrier of V

b is V24() V25() V41() Element of REAL

b * (w - v) is Element of the carrier of V

(a * v) + (b * (w - v)) is Element of the carrier of V

c is V24() V25() V41() Element of REAL

c * (u - v) is Element of the carrier of V

((a * v) + (b * (w - v))) + (c * (u - v)) is Element of the carrier of V

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

b * w is Element of the carrier of V

b * v is Element of the carrier of V

(b * w) - (b * v) is Element of the carrier of V

- (b * v) is Element of the carrier of V

K196(V,(b * w),(- (b * v))) is Element of the carrier of V

(a * v) + ((b * w) - (b * v)) is Element of the carrier of V

((a * v) + ((b * w) - (b * v))) + (c * (u - v)) is Element of the carrier of V

(b * w) + (- (b * v)) is Element of the carrier of V

(a * v) + ((b * w) + (- (b * v))) is Element of the carrier of V

c * u is Element of the carrier of V

c * v is Element of the carrier of V

(c * u) - (c * v) is Element of the carrier of V

- (c * v) is Element of the carrier of V

K196(V,(c * u),(- (c * v))) is Element of the carrier of V

((a * v) + ((b * w) + (- (b * v)))) + ((c * u) - (c * v)) is Element of the carrier of V

(a * v) + (- (b * v)) is Element of the carrier of V

((a * v) + (- (b * v))) + (b * w) is Element of the carrier of V

(- (c * v)) + (c * u) is Element of the carrier of V

(((a * v) + (- (b * v))) + (b * w)) + ((- (c * v)) + (c * u)) is Element of the carrier of V

(b * w) + ((- (c * v)) + (c * u)) is Element of the carrier of V

((a * v) + (- (b * v))) + ((b * w) + ((- (c * v)) + (c * u))) is Element of the carrier of V

(b * w) + (c * u) is Element of the carrier of V

(- (c * v)) + ((b * w) + (c * u)) is Element of the carrier of V

((a * v) + (- (b * v))) + ((- (c * v)) + ((b * w) + (c * u))) is Element of the carrier of V

((a * v) + (- (b * v))) + (- (c * v)) is Element of the carrier of V

(((a * v) + (- (b * v))) + (- (c * v))) + ((b * w) + (c * u)) is Element of the carrier of V

b * (- v) is Element of the carrier of V

(a * v) + (b * (- v)) is Element of the carrier of V

((a * v) + (b * (- v))) + (- (c * v)) is Element of the carrier of V

(((a * v) + (b * (- v))) + (- (c * v))) + ((b * w) + (c * u)) is Element of the carrier of V

- b is V24() V25() V41() Element of REAL

(- b) * v is Element of the carrier of V

(a * v) + ((- b) * v) is Element of the carrier of V

((a * v) + ((- b) * v)) + (- (c * v)) is Element of the carrier of V

(((a * v) + ((- b) * v)) + (- (c * v))) + ((b * w) + (c * u)) is Element of the carrier of V

c * (- v) is Element of the carrier of V

((a * v) + ((- b) * v)) + (c * (- v)) is Element of the carrier of V

(((a * v) + ((- b) * v)) + (c * (- v))) + ((b * w) + (c * u)) is Element of the carrier of V

- c is V24() V25() V41() Element of REAL

(- c) * v is Element of the carrier of V

((a * v) + ((- b) * v)) + ((- c) * v) is Element of the carrier of V

(((a * v) + ((- b) * v)) + ((- c) * v)) + ((b * w) + (c * u)) is Element of the carrier of V

a + (- b) is V24() V25() V41() Element of REAL

(a + (- b)) * v is Element of the carrier of V

((a + (- b)) * v) + ((- c) * v) is Element of the carrier of V

(((a + (- b)) * v) + ((- c) * v)) + ((b * w) + (c * u)) is Element of the carrier of V

(a + (- b)) + (- c) is V24() V25() V41() Element of REAL

((a + (- b)) + (- c)) * v is Element of the carrier of V

(((a + (- b)) + (- c)) * v) + ((b * w) + (c * u)) is Element of the carrier of V

(((a + (- b)) + (- c)) * v) + (b * w) is Element of the carrier of V

((((a + (- b)) + (- c)) * v) + (b * w)) + (c * u) is Element of the carrier of V

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

u is Element of the carrier of V

{v,w,u} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

u + v is Element of the carrier of V

{v,w,(u + v)} is V26() Element of K32( the carrier of V)

a is V24() V25() V41() Element of REAL

a * v is Element of the carrier of V

b is V24() V25() V41() Element of REAL

b * w is Element of the carrier of V

(a * v) + (b * w) is Element of the carrier of V

c is V24() V25() V41() Element of REAL

c * (u + v) is Element of the carrier of V

((a * v) + (b * w)) + (c * (u + v)) is Element of the carrier of V

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

c * v is Element of the carrier of V

c * u is Element of the carrier of V

(c * v) + (c * u) is Element of the carrier of V

((a * v) + (b * w)) + ((c * v) + (c * u)) is Element of the carrier of V

(b * w) + ((c * v) + (c * u)) is Element of the carrier of V

(a * v) + ((b * w) + ((c * v) + (c * u))) is Element of the carrier of V

(b * w) + (c * u) is Element of the carrier of V

(c * v) + ((b * w) + (c * u)) is Element of the carrier of V

(a * v) + ((c * v) + ((b * w) + (c * u))) is Element of the carrier of V

(a * v) + (c * v) is Element of the carrier of V

((a * v) + (c * v)) + ((b * w) + (c * u)) is Element of the carrier of V

a + c is V24() V25() V41() Element of REAL

(a + c) * v is Element of the carrier of V

((a + c) * v) + ((b * w) + (c * u)) is Element of the carrier of V

((a + c) * v) + (b * w) is Element of the carrier of V

(((a + c) * v) + (b * w)) + (c * u) is Element of the carrier of V

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

w + v is Element of the carrier of V

u is Element of the carrier of V

{v,w,u} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

u + v is Element of the carrier of V

{v,(w + v),(u + v)} is V26() Element of K32( the carrier of V)

a is V24() V25() V41() Element of REAL

a * v is Element of the carrier of V

b is V24() V25() V41() Element of REAL

b * (w + v) is Element of the carrier of V

(a * v) + (b * (w + v)) is Element of the carrier of V

c is V24() V25() V41() Element of REAL

c * (u + v) is Element of the carrier of V

((a * v) + (b * (w + v))) + (c * (u + v)) is Element of the carrier of V

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

b * v is Element of the carrier of V

b * w is Element of the carrier of V

(b * v) + (b * w) is Element of the carrier of V

(a * v) + ((b * v) + (b * w)) is Element of the carrier of V

((a * v) + ((b * v) + (b * w))) + (c * (u + v)) is Element of the carrier of V

(a * v) + (b * v) is Element of the carrier of V

((a * v) + (b * v)) + (b * w) is Element of the carrier of V

(((a * v) + (b * v)) + (b * w)) + (c * (u + v)) is Element of the carrier of V

a + b is V24() V25() V41() Element of REAL

(a + b) * v is Element of the carrier of V

((a + b) * v) + (b * w) is Element of the carrier of V

(((a + b) * v) + (b * w)) + (c * (u + v)) is Element of the carrier of V

c * v is Element of the carrier of V

c * u is Element of the carrier of V

(c * v) + (c * u) is Element of the carrier of V

(((a + b) * v) + (b * w)) + ((c * v) + (c * u)) is Element of the carrier of V

(b * w) + ((c * v) + (c * u)) is Element of the carrier of V

((a + b) * v) + ((b * w) + ((c * v) + (c * u))) is Element of the carrier of V

(b * w) + (c * u) is Element of the carrier of V

(c * v) + ((b * w) + (c * u)) is Element of the carrier of V

((a + b) * v) + ((c * v) + ((b * w) + (c * u))) is Element of the carrier of V

((a + b) * v) + (c * v) is Element of the carrier of V

(((a + b) * v) + (c * v)) + ((b * w) + (c * u)) is Element of the carrier of V

(a + b) + c is V24() V25() V41() Element of REAL

((a + b) + c) * v is Element of the carrier of V

(((a + b) + c) * v) + ((b * w) + (c * u)) is Element of the carrier of V

(((a + b) + c) * v) + (b * w) is Element of the carrier of V

((((a + b) + c) * v) + (b * w)) + (c * u) is Element of the carrier of V

V is V24() V25() V41() Element of REAL

v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of v is non empty set

w is Element of the carrier of v

u is Element of the carrier of v

a is Element of the carrier of v

{w,u,a} is V26() Element of K32( the carrier of v)

K32( the carrier of v) is set

V * a is Element of the carrier of v

{w,u,(V * a)} is V26() Element of K32( the carrier of v)

b is V24() V25() V41() Element of REAL

b * w is Element of the carrier of v

c is V24() V25() V41() Element of REAL

c * u is Element of the carrier of v

(b * w) + (c * u) is Element of the carrier of v

r3 is V24() V25() V41() Element of REAL

r3 * (V * a) is Element of the carrier of v

((b * w) + (c * u)) + (r3 * (V * a)) is Element of the carrier of v

0. v is V52(v) Element of the carrier of v

r3 * V is V24() V25() V41() Element of REAL

(r3 * V) * a is Element of the carrier of v

((b * w) + (c * u)) + ((r3 * V) * a) is Element of the carrier of v

V is V24() V25() V41() Element of REAL

v is V24() V25() V41() Element of REAL

w is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of w is non empty set

u is Element of the carrier of w

a is Element of the carrier of w

V * a is Element of the carrier of w

b is Element of the carrier of w

{u,a,b} is V26() Element of K32( the carrier of w)

K32( the carrier of w) is set

v * b is Element of the carrier of w

{u,(V * a),(v * b)} is V26() Element of K32( the carrier of w)

c is V24() V25() V41() Element of REAL

c * u is Element of the carrier of w

r3 is V24() V25() V41() Element of REAL

r3 * (V * a) is Element of the carrier of w

(c * u) + (r3 * (V * a)) is Element of the carrier of w

r4 is V24() V25() V41() Element of REAL

r4 * (v * b) is Element of the carrier of w

((c * u) + (r3 * (V * a))) + (r4 * (v * b)) is Element of the carrier of w

0. w is V52(w) Element of the carrier of w

r3 * V is V24() V25() V41() Element of REAL

(r3 * V) * a is Element of the carrier of w

(c * u) + ((r3 * V) * a) is Element of the carrier of w

((c * u) + ((r3 * V) * a)) + (r4 * (v * b)) is Element of the carrier of w

r4 * v is V24() V25() V41() Element of REAL

(r4 * v) * b is Element of the carrier of w

((c * u) + ((r3 * V) * a)) + ((r4 * v) * b) is Element of the carrier of w

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

u is Element of the carrier of V

{v,w,u} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

- u is Element of the carrier of V

{v,w,(- u)} is V26() Element of K32( the carrier of V)

(- 1) * u is Element of the carrier of V

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

- w is Element of the carrier of V

u is Element of the carrier of V

{v,w,u} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

- u is Element of the carrier of V

{v,(- w),(- u)} is V26() Element of K32( the carrier of V)

(- 1) * u is Element of the carrier of V

(- 1) * w is Element of the carrier of V

V is V24() V25() V41() Element of REAL

v is V24() V25() V41() Element of REAL

w is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of w is non empty set

u is Element of the carrier of w

V * u is Element of the carrier of w

v * u is Element of the carrier of w

a is Element of the carrier of w

{(V * u),(v * u),a} is V26() Element of K32( the carrier of w)

K32( the carrier of w) is set

{(V * u),(v * u)} is V26() Element of K32( the carrier of w)

V is V24() V25() V41() Element of REAL

v is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of v is non empty set

w is Element of the carrier of v

V * w is Element of the carrier of v

u is Element of the carrier of v

{w,(V * w),u} is V26() Element of K32( the carrier of v)

K32( the carrier of v) is set

1 * w is Element of the carrier of v

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

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

v is Element of the carrier of V

{v} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

Lin {v} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V

w is Element of the carrier of V

{w} is V26() Element of K32( the carrier of V)

Lin {w} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V

u is V24() V25() V41() Element of REAL

u * w is Element of the carrier of V

a is Element of the carrier of V

b is V24() V25() V41() Element of REAL

b * v is Element of the carrier of V

b * u is V24() V25() V41() Element of REAL

(b * u) * w is Element of the carrier of V

b is V24() V25() V41() Element of REAL

b * w is Element of the carrier of V

u " is V24() V25() V41() Element of REAL

(u ") * v is Element of the carrier of V

(u ") * u is V24() V25() V41() Element of REAL

((u ") * u) * w is Element of the carrier of V

1 * w is Element of the carrier of V

b * (u ") is V24() V25() V41() Element of REAL

(b * (u ")) * v is Element of the carrier of V

V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

{v,w} is V26() Element of K32( the carrier of V)

K32( the carrier of V) is set

Lin {v,w} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V

u is Element of the carrier of V

a is Element of the carrier of V

{u,a} is V26() Element of K32( the carrier of V)

Lin {u,a} is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V

b is V24() V25() V41() Element of REAL

b * u is Element of the carrier of V

c is V24() V25() V41() Element of REAL

c * a is Element of the carrier of V

(b * u) + (c * a) is Element of the carrier of V

r3 is V24() V25() V41() Element of REAL

r3 * u is Element of the carrier of V

r4 is V24() V25() V41() Element of REAL

r4 * a is Element of the carrier of V

(r3 * u) + (r4 * a) is Element of the carrier of V

b * r4 is V24() V25() V41() Element of REAL

c * r3 is V24() V25() V41() Element of REAL

(b * r4) - (c * r3) is V24() V25() V41() Element of REAL

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

0 * a is Element of the carrier of V

(0. V) + (0 * a) is Element of the carrier of V

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

b " is V24() V25() V41() Element of REAL

(b ") * b is V24() V25() V41() Element of REAL

((b ") * b) * r4 is V24() V25() V41() Element of REAL

(b ") * (c * r3) is V24() V25() V41() Element of REAL

1 * r4 is V24() V25() V41() Element of REAL

(b ") * c is V24() V25() V41() Element of REAL

r3 * ((b ") * c) is V24() V25() V41() Element of REAL

(r3 * ((b ") * c)) * a is Element of the carrier of V

(r3 * u) + ((r3 * ((b ") * c)) * a) is Element of the carrier of V

((b ") * c) * a is Element of the carrier of V

r3 * (((b ") * c) * a) is Element of the carrier of V

(r3 * u) + (r3 * (((b ") * c) * a)) is Element of the carrier of V

u + (((b ") * c) * a) is Element of the carrier of V

r3 * 1 is V24() V25() V41() Element of REAL

(r3 * 1) * (u + (((b ") * c) * a)) is Element of the carrier of V

r3 * ((b ") * b) is V24() V25() V41() Element of REAL

(r3 * ((b ") * b)) * (u + (((b ") * c) * a)) is Element of the carrier of V

r3 * (b ") is V24() V25() V41() Element of REAL

(r3 * (b ")) * b is V24() V25() V41() Element of REAL

((r3 * (b ")) * b) * (u + (((b ") * c) * a)) is Element of the carrier of V

b * (u + (((b ") * c) * a)) is Element of the carrier of V

(r3 * (b ")) * (b * (u + (((b ") * c) * a))) is Element of the carrier of V

b * (((b ") * c) * a) is Element of the carrier of V

(b * u) + (b * (((b ") * c) * a)) is Element of the carrier of V

(r3 * (b ")) * ((b * u) + (b * (((b ") * c) * a))) is Element of the carrier of V

b * ((b ") * c) is V24() V25() V41() Element of REAL

(b * ((b ") * c)) * a is Element of the carrier of V

(b * u) + ((b * ((b ") * c)) * a) is Element of the carrier of V

(r3 * (b ")) * ((b * u) + ((b * ((b ") * c)) * a)) is Element of the carrier of V

b * (b ") is V24() V25() V41() Element of REAL

(b * (b ")) * c is V24() V25() V41() Element of REAL

((b * (b ")) * c) * a is Element of the carrier of V

(b * u) + (((b * (b ")) * c) * a) is Element of the carrier of V

(r3 * (b "))