for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace)
for W1, W2 being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) holds the carrier of W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) c= the carrier of (W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ;

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace)
for W1, W2 being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) st V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) is_the_direct_sum_of W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ,W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) holds
for v, v1, v2 being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) & v2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) & v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + v2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) holds
v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) |-- (W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ,W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of [: the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) = [v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ;

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace)
for W1, W2 being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) st V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) is_the_direct_sum_of W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ,W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) holds
for v, v1, v2 being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) |-- (W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ,W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of [: the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) = [v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) holds
v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + v2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace)
for W1, W2 being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) st V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) is_the_direct_sum_of W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ,W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) holds
for v, v1, v2 being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) |-- (W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ,W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of [: the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) = [v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) holds
( v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) & v2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) ;

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace)
for W1, W2 being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) st V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) is_the_direct_sum_of W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ,W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) holds
for v, v1, v2 being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) |-- (W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ,W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of [: the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) = [v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) holds
v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) |-- (W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ,W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of [: the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) = [v2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ,v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ;

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace)
for W1, W2 being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) st V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) is_the_direct_sum_of W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ,W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) holds
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) holds
v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) |-- (W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ,W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of [: the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) = [v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ,(0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( ) ( V83(b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) left_complementable right_complementable complementable ) Element of the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ;

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace)
for W1, W2 being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) st V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) is_the_direct_sum_of W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ,W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) holds
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) holds
v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) |-- (W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ,W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of [: the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) = [(0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( ) ( V83(b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) left_complementable right_complementable complementable ) Element of the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ;

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace)
for V1 being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) )
for W1 being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of V1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) )
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₂ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) holds
v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) is ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ;

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace)
for V1, V2, W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) )
for W1, W2 being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) st W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₄ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) = V1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) & W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₄ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) = V2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) holds
W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₄ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) + W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₄ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₄ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) = V1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + V2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ;

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) )
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for w being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = w : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
Lin {w : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₂ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₂ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) = Lin {v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ;

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace)
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for X being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) st not v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) holds
for y being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of X : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) & W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) = X : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) holds
X : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) is_the_direct_sum_of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) , Lin {y : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of (b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) ;

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace)
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for X being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) )
for y being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of X : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) & X : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) = W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) & not v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) holds
y : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) |-- (W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) ,(Lin {y : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of (b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) ) : ( ( ) ( ) Element of [: the carrier of (b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) , the carrier of (b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) = [(0. W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) ) : ( ( ) ( V83(b₅ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) ) left_complementable right_complementable complementable ) Element of the carrier of b₅ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of [: the carrier of b₅ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( ) ( non empty ) set ) , the carrier of (b₃ : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) + (Lin {b₂ : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) Subspace of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) ) ;