:: RLSUB_1 semantic presentation

begin

definition
let V be ( ( 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 V106() ) RealLinearSpace) ;
let V1 be ( ( ) ( ) Subset of ) ;
attr V1 is linearly-closed means :: RLSUB_1:def 1
( ( for v, u being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( ) set ) ) st v : ( ( ) ( V31() real V33() ) Real) in V1 : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) & u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in V1 : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) holds
v : ( ( ) ( V31() real V33() ) Real) + u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) ) in V1 : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) ) & ( for a being ( ( ) ( V31() real V33() ) Real)
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( ) set ) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in V1 : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) holds
a : ( ( ) ( V31() real V33() ) Real) * v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) ) in V1 : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) ) );
end;

theorem :: RLSUB_1:1
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 V106() ) RealLinearSpace)
for V1 being ( ( ) ( ) Subset of ) st V1 : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V33() ) set ) & V1 : ( ( ) ( ) Subset of ) is linearly-closed holds
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 V106() ) RealLinearSpace) : ( ( ) ( V55(b1 : ( ( 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 V106() ) RealLinearSpace) ) left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in V1 : ( ( ) ( ) Subset of ) ;

theorem :: RLSUB_1:2
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 V106() ) RealLinearSpace)
for V1 being ( ( ) ( ) Subset of ) st V1 : ( ( ) ( ) Subset of ) is linearly-closed 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 V1 : ( ( ) ( ) Subset of ) holds
- v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in V1 : ( ( ) ( ) Subset of ) ;

theorem :: RLSUB_1:3
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 V106() ) RealLinearSpace)
for V1 being ( ( ) ( ) Subset of ) st V1 : ( ( ) ( ) Subset of ) is linearly-closed holds
for v, u being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in V1 : ( ( ) ( ) Subset of ) & u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in V1 : ( ( ) ( ) Subset of ) holds
v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in V1 : ( ( ) ( ) Subset of ) ;

theorem :: RLSUB_1:4
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 V106() ) RealLinearSpace) holds {(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 V106() ) RealLinearSpace) ) : ( ( ) ( V55(b1 : ( ( 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 V106() ) RealLinearSpace) ) left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is linearly-closed ;

theorem :: RLSUB_1:5
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 V106() ) RealLinearSpace)
for V1 being ( ( ) ( ) Subset of ) st the carrier 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) = V1 : ( ( ) ( ) Subset of ) holds
V1 : ( ( ) ( ) Subset of ) is linearly-closed ;

theorem :: RLSUB_1:6
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 V106() ) RealLinearSpace)
for V1, V2, V3 being ( ( ) ( ) Subset of ) st V1 : ( ( ) ( ) Subset of ) is linearly-closed & V2 : ( ( ) ( ) Subset of ) is linearly-closed & V3 : ( ( ) ( ) Subset of ) = { (v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) where v, u is ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in V1 : ( ( ) ( ) Subset of ) & u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in V2 : ( ( ) ( ) Subset of ) ) } holds
V3 : ( ( ) ( ) Subset of ) is linearly-closed ;

theorem :: RLSUB_1:7
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 V106() ) RealLinearSpace)
for V1, V2 being ( ( ) ( ) Subset of ) st V1 : ( ( ) ( ) Subset of ) is linearly-closed & V2 : ( ( ) ( ) Subset of ) is linearly-closed holds
V1 : ( ( ) ( ) Subset of ) /\ V2 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is linearly-closed ;

definition
let V be ( ( 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 V106() ) RealLinearSpace) ;
mode 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 V106() ) RealLinearSpace) means :: RLSUB_1:def 2
( the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) c= the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) & 0. it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) Element of the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) ) = 0. V : ( ( ) ( ) RLSStruct ) : ( ( ) ( V55(V : ( ( ) ( ) RLSStruct ) ) ) Element of the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) ) & the addF of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( Function-like V18([: the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) ) ) ( Relation-like [: the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) -valued Function-like V18([: the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = the addF of V : ( ( ) ( ) RLSStruct ) : ( ( Function-like V18([: the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) ) ) ( Relation-like [: the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) -valued Function-like V18([: the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) || the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) : ( ( ) ( Relation-like Function-like ) set ) & the Mult of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V36() ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V36() ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = the Mult of V : ( ( ) ( ) RLSStruct ) : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V36() ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V36() ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) | [:REAL : ( ( ) ( non empty V36() ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) );
end;

theorem :: RLSUB_1:8
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 V106() ) RealLinearSpace)
for x being ( ( ) ( ) set )
for W1, W2 being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) st x : ( ( ) ( ) set ) in W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) & W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) is ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) holds
x : ( ( ) ( ) set ) in W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:9
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 V106() ) RealLinearSpace)
for x being ( ( ) ( ) set )
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) st x : ( ( ) ( ) set ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) holds
x : ( ( ) ( ) set ) in 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 V106() ) RealLinearSpace) ;

theorem :: RLSUB_1:10
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 V106() ) RealLinearSpace)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) )
for w being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds w : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) is ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ;

theorem :: RLSUB_1:11
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 V106() ) RealLinearSpace)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) holds 0. W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( V55(b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) left_complementable right_complementable complementable ) Element of the carrier of b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( 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 V106() ) RealLinearSpace) : ( ( ) ( V55(b1 : ( ( 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 V106() ) RealLinearSpace) ) left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLSUB_1:12
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 V106() ) 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 V106() ) 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 V106() ) RealLinearSpace) ) holds 0. W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( V55(b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) left_complementable right_complementable complementable ) Element of the carrier of b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ) = 0. W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( V55(b3 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) left_complementable right_complementable complementable ) Element of the carrier of b3 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLSUB_1:13
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 V106() ) RealLinearSpace)
for v, u 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 V106() ) 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 V106() ) RealLinearSpace) )
for w1, w2 being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st w1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) & w2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
w1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + w2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b4 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLSUB_1:14
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 V106() ) RealLinearSpace)
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V31() real V33() ) Real)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) )
for w being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st w : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( V31() real V33() ) Real) * w : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b4 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ) = a : ( ( ) ( V31() real V33() ) Real) * v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLSUB_1:15
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 V106() ) RealLinearSpace)
for v 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 V106() ) 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 V106() ) RealLinearSpace) )
for w being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st w : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
- v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = - w : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b3 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLSUB_1:16
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 V106() ) RealLinearSpace)
for v, u 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 V106() ) 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 V106() ) RealLinearSpace) )
for w1, w2 being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st w1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) & w2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
w1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - w2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b4 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLSUB_1:17
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 V106() ) RealLinearSpace)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) holds 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 V106() ) RealLinearSpace) : ( ( ) ( V55(b1 : ( ( 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 V106() ) RealLinearSpace) ) left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:18
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 V106() ) 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 V106() ) 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 V106() ) RealLinearSpace) ) holds 0. W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( V55(b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) left_complementable right_complementable complementable ) Element of the carrier of b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:19
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 V106() ) RealLinearSpace)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) holds 0. W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( V55(b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) left_complementable right_complementable complementable ) Element of the carrier of b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ) in 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 V106() ) RealLinearSpace) ;

theorem :: RLSUB_1:20
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 V106() ) RealLinearSpace)
for u, v 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 V106() ) 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 V106() ) RealLinearSpace) ) st u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) & v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) holds
u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:21
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 V106() ) RealLinearSpace)
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V31() real V33() ) Real)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) holds
a : ( ( ) ( V31() real V33() ) Real) * v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:22
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 V106() ) RealLinearSpace)
for v 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 V106() ) 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 V106() ) RealLinearSpace) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) holds
- v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:23
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 V106() ) RealLinearSpace)
for u, v 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 V106() ) 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 V106() ) RealLinearSpace) ) st u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) & v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) holds
u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:24
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 V106() ) RealLinearSpace)
for V1 being ( ( ) ( ) Subset of )
for D being ( ( non empty ) ( non empty ) set )
for d1 being ( ( ) ( ) Element of D : ( ( non empty ) ( non empty ) set ) )
for A being ( ( Function-like V18([:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like V18([:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) BinOp of D : ( ( non empty ) ( non empty ) set ) )
for M being ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V36() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) Function of [:REAL : ( ( ) ( non empty V36() ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) ) st V1 : ( ( ) ( ) Subset of ) = D : ( ( non empty ) ( non empty ) set ) & d1 : ( ( ) ( ) Element of b3 : ( ( non empty ) ( 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 V106() ) RealLinearSpace) : ( ( ) ( V55(b1 : ( ( 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 V106() ) RealLinearSpace) ) left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) & A : ( ( Function-like V18([:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like V18([:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) BinOp of b3 : ( ( non empty ) ( non empty ) set ) ) = the addF 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 V106() ) RealLinearSpace) : ( ( Function-like V18([: the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18([: the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) || V1 : ( ( ) ( ) Subset of ) : ( ( ) ( Relation-like Function-like ) set ) & M : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V36() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) Function of [:REAL : ( ( ) ( non empty V36() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) = the Mult 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 V106() ) RealLinearSpace) : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() ) set ) , the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() ) set ) , the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V36() ) set ) , the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V36() ) set ) , the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) | [:REAL : ( ( ) ( non empty V36() ) set ) ,V1 : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) holds
RLSStruct(# D : ( ( non empty ) ( non empty ) set ) ,d1 : ( ( ) ( ) Element of b3 : ( ( non empty ) ( non empty ) set ) ) ,A : ( ( Function-like V18([:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like V18([:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) BinOp of b3 : ( ( non empty ) ( non empty ) set ) ) ,M : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V36() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) Function of [:REAL : ( ( ) ( non empty V36() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) is ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:25
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 V106() ) RealLinearSpace) holds 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 V106() ) RealLinearSpace) is ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:26
for V, X being ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) st V : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) is ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of X : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) & X : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) is ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of V : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) holds
V : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) = X : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ;

theorem :: RLSUB_1:27
for V, X, Y 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 V106() ) 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 V106() ) RealLinearSpace) is ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of X : ( ( 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 V106() ) RealLinearSpace) ) & X : ( ( 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 V106() ) RealLinearSpace) is ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of Y : ( ( 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 V106() ) RealLinearSpace) ) holds
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 V106() ) RealLinearSpace) is ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of Y : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:28
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 V106() ) 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 V106() ) 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 V106() ) RealLinearSpace) ) st the carrier of W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) c= the carrier of W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) holds
W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) is ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:29
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 V106() ) 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 V106() ) 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 V106() ) RealLinearSpace) ) st ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) holds
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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) holds
W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) is ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

registration
let V be ( ( 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 V106() ) RealLinearSpace) ;
cluster non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() for ( ( ) ( ) 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 V106() ) RLSStruct ) ) ;
end;

theorem :: RLSUB_1:30
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 V106() ) RealLinearSpace)
for W1, W2 being ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) st the carrier of W1 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) = the carrier of W2 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) holds
W1 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) = W2 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:31
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 V106() ) RealLinearSpace)
for W1, W2 being ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) st ( for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W1 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) iff v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W2 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ) holds
W1 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) = W2 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:32
for V being ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for W being ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of V : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) st the carrier of W : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) = the carrier of V : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) holds
W : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) = V : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ;

theorem :: RLSUB_1:33
for V being ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for W being ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of V : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) st ( for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) iff v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in V : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) holds
W : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) = V : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ;

theorem :: RLSUB_1:34
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 V106() ) RealLinearSpace)
for V1 being ( ( ) ( ) Subset of )
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) st the carrier of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) = V1 : ( ( ) ( ) Subset of ) holds
V1 : ( ( ) ( ) Subset of ) is linearly-closed ;

theorem :: RLSUB_1:35
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 V106() ) RealLinearSpace)
for V1 being ( ( ) ( ) Subset of ) st V1 : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V33() ) set ) & V1 : ( ( ) ( ) Subset of ) is linearly-closed holds
ex W being ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) st V1 : ( ( ) ( ) Subset of ) = the carrier of W : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ;

definition
let V be ( ( 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 V106() ) RealLinearSpace) ;
func (0). V -> ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RLSStruct ) ) means :: RLSUB_1:def 3
 the carrier of it : ( ( ) ( ) Element 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 V106() ) RLSStruct ) ) : ( ( ) ( ) 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 V106() ) RLSStruct ) ) : ( ( ) ( V55(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 V106() ) RLSStruct ) ) left_complementable right_complementable complementable ) Element of the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let V be ( ( 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 V106() ) RealLinearSpace) ;
func (Omega). V -> ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RLSStruct ) ) equals :: RLSUB_1:def 4
 RLSStruct(# the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) , the ZeroF 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 V106() ) RLSStruct ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) , the addF 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 V106() ) RLSStruct ) : ( ( Function-like V18([: the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) , the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) , the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V18([: the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) , the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) , the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , the Mult 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 V106() ) RLSStruct ) : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() ) set ) , the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() ) set ) , the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V36() ) set ) , the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V36() ) set ) , the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) ;
end;

theorem :: RLSUB_1:36
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 V106() ) RealLinearSpace)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) holds (0). W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) = (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 V106() ) RealLinearSpace) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:37
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 V106() ) 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 V106() ) 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 V106() ) RealLinearSpace) ) holds (0). W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) = (0). W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b3 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:38
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 V106() ) RealLinearSpace)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) holds (0). W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) is ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:39
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 V106() ) RealLinearSpace)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) holds (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 V106() ) RealLinearSpace) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) is ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:40
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 V106() ) 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 V106() ) 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 V106() ) RealLinearSpace) ) holds (0). W1 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) is ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:41
for V being ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) holds V : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) is ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of (Omega). V : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) ;

definition
let V be ( ( 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 V106() ) RealLinearSpace) ;
let v be ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ;
let W be ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) ;
func v + W -> ( ( ) ( ) Subset of ) equals :: RLSUB_1:def 5
 { (v : ( ( ) ( ) Element 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 V106() ) RLSStruct ) ) + u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier 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 V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) where u is ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( Function-like V18([: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 V106() ) RLSStruct ) ,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 V106() ) RLSStruct ) :] : ( ( ) ( ) set ) ,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 V106() ) RLSStruct ) ) ) ( Relation-like [: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 V106() ) RLSStruct ) ,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 V106() ) RLSStruct ) :] : ( ( ) ( ) set ) -defined 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 V106() ) RLSStruct ) -valued Function-like V18([: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 V106() ) RLSStruct ) ,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 V106() ) RLSStruct ) :] : ( ( ) ( ) set ) ,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 V106() ) RLSStruct ) ) ) Element of bool [:[: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 V106() ) RLSStruct ) ,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 V106() ) RLSStruct ) :] : ( ( ) ( ) set ) ,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 V106() ) RLSStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) } ;
end;

definition
let V be ( ( 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 V106() ) RealLinearSpace) ;
let W be ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) ;
mode Coset of W -> ( ( ) ( ) Subset of ) means :: RLSUB_1:def 6
 ex v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st it : ( ( Function-like V18([: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 V106() ) RLSStruct ) ,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 V106() ) RLSStruct ) :] : ( ( ) ( ) set ) ,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 V106() ) RLSStruct ) ) ) ( Relation-like [: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 V106() ) RLSStruct ) ,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 V106() ) RLSStruct ) :] : ( ( ) ( ) set ) -defined 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 V106() ) RLSStruct ) -valued Function-like V18([: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 V106() ) RLSStruct ) ,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 V106() ) RLSStruct ) :] : ( ( ) ( ) set ) ,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 V106() ) RLSStruct ) ) ) Element of bool [:[: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 V106() ) RLSStruct ) ,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 V106() ) RLSStruct ) :] : ( ( ) ( ) set ) ,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 V106() ) RLSStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( ) Element 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 V106() ) RLSStruct ) ) : ( ( ) ( ) Subset of ) ;
end;

theorem :: RLSUB_1:42
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 V106() ) RealLinearSpace)
for v 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( 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 V106() ) RealLinearSpace) : ( ( ) ( V55(b1 : ( ( 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 V106() ) RealLinearSpace) ) left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) iff v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:43
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 V106() ) RealLinearSpace)
for v 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 V106() ) 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 V106() ) RealLinearSpace) ) holds v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) ;

theorem :: RLSUB_1:44
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 V106() ) RealLinearSpace)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) holds (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 V106() ) RealLinearSpace) ) : ( ( ) ( V55(b1 : ( ( 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 V106() ) RealLinearSpace) ) left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = the carrier of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ;

theorem :: RLSUB_1:45
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 V106() ) RealLinearSpace)
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds 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 V106() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = {v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLSUB_1:46
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 V106() ) RealLinearSpace)
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + ((Omega). 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 V106() ) RealLinearSpace) ) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = the carrier 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ;

theorem :: RLSUB_1:47
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 V106() ) RealLinearSpace)
for v 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( 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 V106() ) RealLinearSpace) : ( ( ) ( V55(b1 : ( ( 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 V106() ) RealLinearSpace) ) left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) iff v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = the carrier of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLSUB_1:48
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 V106() ) RealLinearSpace)
for v 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) iff v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = the carrier of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLSUB_1:49
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 V106() ) RealLinearSpace)
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V31() real V33() ) Real)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) holds
(a : ( ( ) ( V31() real V33() ) Real) * v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = the carrier of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ;

theorem :: RLSUB_1:50
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 V106() ) RealLinearSpace)
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V31() real V33() ) Real)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) st a : ( ( ) ( V31() real V33() ) Real) <> 0 : ( ( ) ( Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V33() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V36() ) set ) : ( ( ) ( non empty ) set ) ) ) & (a : ( ( ) ( V31() real V33() ) Real) * v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = the carrier of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) holds
v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:51
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 V106() ) RealLinearSpace)
for v 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) iff (- v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = the carrier of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLSUB_1:52
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 V106() ) RealLinearSpace)
for u, v 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) iff v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = (v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) ) ;

theorem :: RLSUB_1:53
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 V106() ) RealLinearSpace)
for u, v 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) iff v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = (v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) ) ;

theorem :: RLSUB_1:54
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 V106() ) RealLinearSpace)
for v, u 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in u : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) iff u : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) ) ;

theorem :: RLSUB_1:55
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 V106() ) RealLinearSpace)
for v 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = (- v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) iff v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:56
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 V106() ) RealLinearSpace)
for u, v1, v2 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 V106() ) 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 V106() ) RealLinearSpace) ) st u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v1 : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) & u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v2 : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) holds
v1 : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = v2 : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) ;

theorem :: RLSUB_1:57
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 V106() ) RealLinearSpace)
for u, v 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 V106() ) 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 V106() ) RealLinearSpace) ) st u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) & u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in (- v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) holds
v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:58
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 V106() ) RealLinearSpace)
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V31() real V33() ) Real)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) st a : ( ( ) ( V31() real V33() ) Real) <> 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V31() real V33() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty V36() ) set ) : ( ( ) ( non empty ) set ) ) ) & a : ( ( ) ( V31() real V33() ) Real) * v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) holds
v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:59
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 V106() ) RealLinearSpace)
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V31() real V33() ) Real)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) holds
a : ( ( ) ( V31() real V33() ) Real) * v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) ;

theorem :: RLSUB_1:60
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 V106() ) RealLinearSpace)
for v 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( - v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) iff v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:61
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 V106() ) RealLinearSpace)
for u, v 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) iff u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:62
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 V106() ) RealLinearSpace)
for v, u 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) iff u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:63
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 V106() ) RealLinearSpace)
for u, v 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) iff ex v1 being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st
( v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) & u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: RLSUB_1:64
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 V106() ) RealLinearSpace)
for u, v 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) iff ex v1 being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st
( v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) & u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: RLSUB_1:65
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 V106() ) RealLinearSpace)
for v1, v2 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( ex v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st
( v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) & v2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) ) iff 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 b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:66
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 V106() ) RealLinearSpace)
for v, u 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 V106() ) 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 V106() ) RealLinearSpace) ) st v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = u : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) holds
ex v1 being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st
( v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) & v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLSUB_1:67
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 V106() ) RealLinearSpace)
for v, u 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 V106() ) 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 V106() ) RealLinearSpace) ) st v : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = u : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) holds
ex v1 being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st
( v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) & v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLSUB_1:68
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 V106() ) RealLinearSpace)
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for W1, W2 being ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) holds
( v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W1 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W2 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) iff W1 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) = W2 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:69
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 V106() ) RealLinearSpace)
for v, u being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for W1, W2 being ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) st v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W1 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) = u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W2 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) holds
W1 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) = W2 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:70
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 V106() ) RealLinearSpace)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) )
for C being ( ( ) ( ) Coset of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) holds
( C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) is linearly-closed iff C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) = the carrier of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLSUB_1:71
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 V106() ) RealLinearSpace)
for W1, W2 being ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) )
for C1 being ( ( ) ( ) Coset of W1 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) )
for C2 being ( ( ) ( ) Coset of W2 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) st C1 : ( ( ) ( ) Coset of b2 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) = C2 : ( ( ) ( ) Coset of b3 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) holds
W1 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) = W2 : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ;

theorem :: RLSUB_1:72
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 V106() ) RealLinearSpace)
for v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds {v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Coset of (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 V106() ) RealLinearSpace) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:73
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 V106() ) RealLinearSpace)
for V1 being ( ( ) ( ) Subset of ) st V1 : ( ( ) ( ) Subset of ) is ( ( ) ( ) Coset of (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 V106() ) RealLinearSpace) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) holds
ex v being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st V1 : ( ( ) ( ) Subset of ) = {v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLSUB_1:74
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 V106() ) RealLinearSpace)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) ) holds the carrier of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) is ( ( ) ( ) Coset of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:75
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 V106() ) RealLinearSpace) holds the carrier 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) is ( ( ) ( ) Coset of (Omega). 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 V106() ) RealLinearSpace) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:76
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 V106() ) RealLinearSpace)
for V1 being ( ( ) ( ) Subset of ) st V1 : ( ( ) ( ) Subset of ) is ( ( ) ( ) Coset of (Omega). 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 V106() ) RealLinearSpace) : ( ( strict ) ( non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) holds
V1 : ( ( ) ( ) Subset of ) = the carrier 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ;

theorem :: RLSUB_1:77
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 V106() ) RealLinearSpace)
for W being ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) 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 V106() ) RealLinearSpace) )
for C being ( ( ) ( ) Coset of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) holds
( 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 V106() ) RealLinearSpace) : ( ( ) ( V55(b1 : ( ( 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 V106() ) RealLinearSpace) ) left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) iff C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) = the carrier of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLSUB_1:78
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 V106() ) RealLinearSpace)
for u 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 V106() ) 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 V106() ) RealLinearSpace) )
for C being ( ( ) ( ) Coset of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) holds
( u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b3 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) iff C : ( ( ) ( ) Coset of b3 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) = u : ( ( ) ( 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 V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) : ( ( ) ( ) Subset of ) ) ;

theorem :: RLSUB_1:79
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 V106() ) RealLinearSpace)
for u, v 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 V106() ) 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 V106() ) RealLinearSpace) )
for C being ( ( ) ( ) Coset of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) st u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b4 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) & v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b4 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) holds
ex v1 being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st
( v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) & u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLSUB_1:80
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 V106() ) RealLinearSpace)
for u, v 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 V106() ) 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 V106() ) RealLinearSpace) )
for C being ( ( ) ( ) Coset of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) st u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b4 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) & v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b4 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) holds
ex v1 being ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st
( v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) & u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLSUB_1:81
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 V106() ) RealLinearSpace)
for v1, v2 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 V106() ) 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 V106() ) RealLinearSpace) ) holds
( ex C being ( ( ) ( ) Coset of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) st
( v1 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b4 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) & v2 : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b4 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ) iff 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 b1 : ( ( 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 V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;

theorem :: RLSUB_1:82
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 V106() ) RealLinearSpace)
for u 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 V106() ) 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 V106() ) RealLinearSpace) )
for B, C being ( ( ) ( ) Coset of W : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) st u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in B : ( ( ) ( ) Coset of b3 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) & u : ( ( ) ( left_complementable right_complementable complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b3 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) holds
B : ( ( ) ( ) Coset of b3 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) = C : ( ( ) ( ) Coset of b3 : ( ( ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( 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 V106() ) RealLinearSpace) ) ) ;