:: RLVECT_4 semantic presentation

begin

scheme :: RLVECT_4:sch 1
LambdaSep3{ F1() -> ( ( non empty ) ( non empty ) set ) , F2() -> ( ( non empty ) ( non empty ) set ) , F3() -> ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) , F4() -> ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) , F5() -> ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) , F6() -> ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) , F7() -> ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) , F8() -> ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) , F9( ( ( ) ( ) set ) ) -> ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) } :
ex f being ( ( Function-like quasi_total ) ( V7() V10(F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) V11(F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) Function-like quasi_total ) Function of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ,F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) st
( f : ( ( Function-like quasi_total ) ( V7() V10(F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) V11(F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) Function-like quasi_total ) Function of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ,F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) . F3( ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) = F6( ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( V7() V10(F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) V11(F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) Function-like quasi_total ) Function of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ,F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) . F4( ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) = F7( ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( V7() V10(F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) V11(F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) Function-like quasi_total ) Function of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ,F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) . F5( ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) = F8( ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) & ( for C being ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) st C : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) <> F3( ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) & C : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) <> F4( ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) & C : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) <> F5( ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) holds
f : ( ( Function-like quasi_total ) ( V7() V10(F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) V11(F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) Function-like quasi_total ) Function of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ,F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) . C : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) = F9( ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ,C : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F2( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) )
provided
F3( ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) <> F4( ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) and
F3( ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) <> F5( ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) and
F4( ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) <> F5( ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of F1( ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) set ) )
proof end;

theorem :: RLVECT_4:1
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & (w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & (w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLVECT_4:2
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v1, w, v2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) holds
v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_4:3
for a being ( ( ) ( V24() V25() V41() ) Real)
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds - (a : ( ( ) ( V24() V25() V41() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = (- a : ( ( ) ( V24() V25() V41() ) Real) ) : ( ( ) ( V24() V25() V41() ) Element of REAL : ( ( ) ( non empty V5() V26() ) set ) ) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_4:4
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for W1, W2 being ( ( ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of V : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) st W1 : ( ( ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) is ( ( ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of W2 : ( ( ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) holds
v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + W1 : ( ( ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) c= v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + W2 : ( ( ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: RLVECT_4:5
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for W being ( ( ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of V : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) st u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) holds
v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: RLVECT_4:6
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for l being ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
Sum l : ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = (((l : ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) . u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V24() V25() V41() ) Element of REAL : ( ( ) ( non empty V5() V26() ) set ) ) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + ((l : ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) . v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V24() V25() V41() ) Element of REAL : ( ( ) ( non empty V5() V26() ) set ) ) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + ((l : ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) . w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V24() V25() V41() ) Element of REAL : ( ( ) ( non empty V5() V26() ) set ) ) * w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_4:7
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( ( u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent ) iff for a, b, c being ( ( ) ( V24() V25() V41() ) Real) st ((a : ( ( ) ( V24() V25() V41() ) Real) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + (b : ( ( ) ( V24() V25() V41() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + (c : ( ( ) ( V24() V25() V41() ) Real) * w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = 0. V : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V52(b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( V24() V25() V41() ) Real) = 0 : ( ( ) ( V17() V18() V19() V23() V24() V25() V41() ) Element of NAT : ( ( ) ( non empty V17() V18() V19() ) Element of K32(REAL : ( ( ) ( non empty V5() V26() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( ) ( V24() V25() V41() ) Real) = 0 : ( ( ) ( V17() V18() V19() V23() V24() V25() V41() ) Element of NAT : ( ( ) ( non empty V17() V18() V19() ) Element of K32(REAL : ( ( ) ( non empty V5() V26() ) set ) ) : ( ( ) ( ) set ) ) ) & c : ( ( ) ( V24() V25() V41() ) Real) = 0 : ( ( ) ( V17() V18() V19() V23() V24() V25() V41() ) Element of NAT : ( ( ) ( non empty V17() V18() V19() ) Element of K32(REAL : ( ( ) ( non empty V5() V26() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ;

theorem :: RLVECT_4:8
for x being ( ( ) ( ) set )
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) set ) in Lin {v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) iff ex a being ( ( ) ( V24() V25() V41() ) Real) st x : ( ( ) ( ) set ) = a : ( ( ) ( V24() V25() V41() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLVECT_4:9
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ;

theorem :: RLVECT_4:10
for x being ( ( ) ( ) set )
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) set ) in v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (Lin {w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) : ( ( ) ( ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) iff ex a being ( ( ) ( V24() V25() V41() ) Real) st x : ( ( ) ( ) set ) = v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (a : ( ( ) ( V24() V25() V41() ) Real) * w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLVECT_4:11
for x being ( ( ) ( ) set )
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for w1, w2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) set ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) iff ex a, b being ( ( ) ( V24() V25() V41() ) Real) st x : ( ( ) ( ) set ) = (a : ( ( ) ( V24() V25() V41() ) Real) * w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + (b : ( ( ) ( V24() V25() V41() ) Real) * w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLVECT_4:12
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for w1, w2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) & w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) ;

theorem :: RLVECT_4:13
for x being ( ( ) ( ) set )
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v, w1, w2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) set ) in v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) : ( ( ) ( ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) iff ex a, b being ( ( ) ( V24() V25() V41() ) Real) st x : ( ( ) ( ) set ) = (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (a : ( ( ) ( V24() V25() V41() ) Real) * w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + (b : ( ( ) ( V24() V25() V41() ) Real) * w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLVECT_4:14
for x being ( ( ) ( ) set )
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v1, v2, v3 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) set ) in Lin {v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) iff ex a, b, c being ( ( ) ( V24() V25() V41() ) Real) st x : ( ( ) ( ) set ) = ((a : ( ( ) ( V24() V25() V41() ) Real) * v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + (b : ( ( ) ( V24() V25() V41() ) Real) * v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + (c : ( ( ) ( V24() V25() V41() ) Real) * v3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLVECT_4:15
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for w1, w2, w3 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) & w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) & w3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) ;

theorem :: RLVECT_4:16
for x being ( ( ) ( ) set )
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v, w1, w2, w3 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) set ) in v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) : ( ( ) ( ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) iff ex a, b, c being ( ( ) ( V24() V25() V41() ) Real) st x : ( ( ) ( ) set ) = ((v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (a : ( ( ) ( V24() V25() V41() ) Real) * w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + (b : ( ( ) ( V24() V25() V41() ) Real) * w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + (c : ( ( ) ( V24() V25() V41() ) Real) * w3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLVECT_4:17
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
{u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent ;

theorem :: RLVECT_4:18
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
{u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent ;

theorem :: RLVECT_4:19
for a being ( ( ) ( V24() V25() V41() ) Real)
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( V24() V25() V41() ) Real) <> 0 : ( ( ) ( V17() V18() V19() V23() V24() V25() V41() ) Element of NAT : ( ( ) ( non empty V17() V18() V19() ) Element of K32(REAL : ( ( ) ( non empty V5() V26() ) set ) ) : ( ( ) ( ) set ) ) ) holds
{u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(a : ( ( ) ( V24() V25() V41() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent ;

theorem :: RLVECT_4:20
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
{u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(- v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent ;

theorem :: RLVECT_4:21
for a, b being ( ( ) ( V24() V25() V41() ) Real)
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( V24() V25() V41() ) Real) <> b : ( ( ) ( V24() V25() V41() ) Real) holds
{(a : ( ( ) ( V24() V25() V41() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ,(b : ( ( ) ( V24() V25() V41() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b3 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-dependent ;

theorem :: RLVECT_4:22
for a being ( ( ) ( V24() V25() V41() ) Real)
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( V24() V25() V41() ) Real) <> 1 : ( ( ) ( non empty V17() V18() V19() V23() V24() V25() V41() ) Element of NAT : ( ( ) ( non empty V17() V18() V19() ) Element of K32(REAL : ( ( ) ( non empty V5() V26() ) set ) ) : ( ( ) ( ) set ) ) ) holds
{v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(a : ( ( ) ( V24() V25() V41() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-dependent ;

theorem :: RLVECT_4:23
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, w, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
{u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent ;

theorem :: RLVECT_4:24
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, w, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
{u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ,(v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent ;

theorem :: RLVECT_4:25
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, w, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
{u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent ;

theorem :: RLVECT_4:26
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, w, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
{u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ,(v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent ;

theorem :: RLVECT_4:27
for a being ( ( ) ( V24() V25() V41() ) Real)
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, w, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( V24() V25() V41() ) Real) <> 0 : ( ( ) ( V17() V18() V19() V23() V24() V25() V41() ) Element of NAT : ( ( ) ( non empty V17() V18() V19() ) Element of K32(REAL : ( ( ) ( non empty V5() V26() ) set ) ) : ( ( ) ( ) set ) ) ) holds
{u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(a : ( ( ) ( V24() V25() V41() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent ;

theorem :: RLVECT_4:28
for a, b being ( ( ) ( V24() V25() V41() ) Real)
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, w, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b3 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( V24() V25() V41() ) Real) <> 0 : ( ( ) ( V17() V18() V19() V23() V24() V25() V41() ) Element of NAT : ( ( ) ( non empty V17() V18() V19() ) Element of K32(REAL : ( ( ) ( non empty V5() V26() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( ) ( V24() V25() V41() ) Real) <> 0 : ( ( ) ( V17() V18() V19() V23() V24() V25() V41() ) Element of NAT : ( ( ) ( non empty V17() V18() V19() ) Element of K32(REAL : ( ( ) ( non empty V5() V26() ) set ) ) : ( ( ) ( ) set ) ) ) holds
{u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(a : ( ( ) ( V24() V25() V41() ) Real) * w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ,(b : ( ( ) ( V24() V25() V41() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b3 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent ;

theorem :: RLVECT_4:29
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, w, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
{u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(- v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent ;

theorem :: RLVECT_4:30
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for u, w, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
{u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(- w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ,(- v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent ;

theorem :: RLVECT_4:31
for a, b being ( ( ) ( V24() V25() V41() ) Real)
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( V24() V25() V41() ) Real) <> b : ( ( ) ( V24() V25() V41() ) Real) holds
{(a : ( ( ) ( V24() V25() V41() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ,(b : ( ( ) ( V24() V25() V41() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b3 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-dependent ;

theorem :: RLVECT_4:32
for a being ( ( ) ( V24() V25() V41() ) Real)
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( V24() V25() V41() ) Real) <> 1 : ( ( ) ( non empty V17() V18() V19() V23() V24() V25() V41() ) Element of NAT : ( ( ) ( non empty V17() V18() V19() ) Element of K32(REAL : ( ( ) ( non empty V5() V26() ) set ) ) : ( ( ) ( ) set ) ) ) holds
{v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(a : ( ( ) ( V24() V25() V41() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b2 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-dependent ;

theorem :: RLVECT_4:33
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> 0. V : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V52(b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) holds
Lin {v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) = Lin {w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ;

theorem :: RLVECT_4:34
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v1, v2, w1, w2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & {v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) & v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) holds
( Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) = Lin {v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) Subspace of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) & {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLVECT_4:35
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for w, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> 0. V : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( V52(b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) & {v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-dependent holds
ex a being ( ( ) ( V24() V25() V41() ) Real) st v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = a : ( ( ) ( V24() V25() V41() ) Real) * w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_4:36
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v, w, u being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & {v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-independent & {u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is linearly-dependent holds
ex a, b being ( ( ) ( V24() V25() V41() ) Real) st u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = (a : ( ( ) ( V24() V25() V41() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + (b : ( ( ) ( V24() V25() V41() ) Real) * w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_4:37
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V24() V25() V41() ) Real) ex l being ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st l : ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) . v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V25() V41() ) Element of REAL : ( ( ) ( non empty V5() V26() ) set ) ) = a : ( ( ) ( V24() V25() V41() ) Real) ;

theorem :: RLVECT_4:38
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v1, v2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( V24() V25() V41() ) Real) st v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
ex l being ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st
( l : ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) . v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V25() V41() ) Element of REAL : ( ( ) ( non empty V5() V26() ) set ) ) = a : ( ( ) ( V24() V25() V41() ) Real) & l : ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) . v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V25() V41() ) Element of REAL : ( ( ) ( non empty V5() V26() ) set ) ) = b : ( ( ) ( V24() V25() V41() ) Real) ) ;

theorem :: RLVECT_4:39
for V being ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace)
for v1, v2, v3 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for a, b, c being ( ( ) ( V24() V25() V41() ) Real) st v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
ex l being ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) st
( l : ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) . v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V25() V41() ) Element of REAL : ( ( ) ( non empty V5() V26() ) set ) ) = a : ( ( ) ( V24() V25() V41() ) Real) & l : ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) . v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V25() V41() ) Element of REAL : ( ( ) ( non empty V5() V26() ) set ) ) = b : ( ( ) ( V24() V25() V41() ) Real) & l : ( ( ) ( V7() V10( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) V11( REAL : ( ( ) ( non empty V5() V26() ) set ) ) Function-like quasi_total ) Linear_Combination of {b2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( V26() ) Element of K32( the carrier of b1 : ( ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) . v3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V25() V41() ) Element of REAL : ( ( ) ( non empty V5() V26() ) set ) ) = c : ( ( ) ( V24() V25() V41() ) Real) ) ;