:: RUSUB_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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ;
mode Subspace of V -> ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) means :: RUSUB_1:def 1
( the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) c= the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) & 0. it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) Element of the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) ) = 0. V : ( ( ) ( ) UNITSTR ) : ( ( ) ( V55(V : ( ( ) ( ) UNITSTR ) ) ) Element of the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) ) & the addF of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( Function-like V18([: the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) ) ) ( Relation-like [: the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) -valued Function-like V18([: the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = the addF of V : ( ( ) ( ) UNITSTR ) : ( ( Function-like V18([: the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) ) ) ( Relation-like [: the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) -valued Function-like V18([: the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) || the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) : ( ( ) ( Relation-like Function-like ) set ) & the Mult of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = the Mult of V : ( ( ) ( ) UNITSTR ) : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) | [:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) & the scalar of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( Function-like V18([: the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) ) ( Relation-like [: the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) -valued Function-like V18([: the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) V119() V120() V121() ) Element of bool [:[: the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) :] : ( ( ) ( V119() V120() V121() ) set ) : ( ( ) ( non empty ) set ) ) = the scalar of V : ( ( ) ( ) UNITSTR ) : ( ( Function-like V18([: the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) ) ( Relation-like [: the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) -valued Function-like V18([: the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) V119() V120() V121() ) Element of bool [:[: the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) :] : ( ( ) ( V119() V120() V121() ) set ) : ( ( ) ( non empty ) set ) ) || the carrier of it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( ) ( ) set ) : ( ( ) ( Relation-like Function-like ) set ) );
end;

theorem :: RUSUB_1:1
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2 being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in W1 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & W1 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
x : ( ( ) ( ) set ) in W2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:2
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds
x : ( ( ) ( ) set ) in V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ;

theorem :: RUSUB_1:3
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for w being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds w : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) is ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_1:4
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds 0. W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( V55(b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) right_complementable ) Element of the carrier of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) = 0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( V55(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_1:5
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2 being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds 0. W1 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( V55(b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) right_complementable ) Element of the carrier of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) = 0. W2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( V55(b3 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) right_complementable ) Element of the carrier of b3 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_1:6
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for w1, w2 being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st w1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) & w2 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
w1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + w2 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_1:7
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for w being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( ext-real V34() real ) Real) st w : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ext-real V34() real ) Real) * w : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ext-real V34() real ) Real) * v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_1:8
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v1, v2 being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for w1, w2 being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st w1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) & w2 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v2 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
w1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) .|. w2 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) = v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) .|. v2 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) ;

theorem :: RUSUB_1:9
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for w being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st w : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
- v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) = - w : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_1:10
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for w1, w2 being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st w1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) & w2 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
w1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - w2 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_1:11
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds 0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( V55(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:12
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2 being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds 0. W1 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( V55(b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) right_complementable ) Element of the carrier of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) in W2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:13
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds 0. W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( V55(b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) right_complementable ) Element of the carrier of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) in V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ;

theorem :: RUSUB_1:14
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds
u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:15
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( ext-real V34() real ) Real) st v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds
a : ( ( ) ( ext-real V34() real ) Real) * v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:16
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds
- v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:17
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds
u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:18
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
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() V129() V130() V131() V135() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) 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() V129() V130() V131() V135() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) Function of [:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) )
for S being ( ( Function-like V18([:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) ) ( Relation-like [:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) -valued Function-like V18([:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) V119() V120() V121() ) Function of [:D : ( ( non empty ) ( non empty ) set ) ,D : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( V55(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( Function-like V18([: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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() V129() V130() V131() V135() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) 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() V129() V130() V131() V135() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) Function of [:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) | [:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ,V1 : ( ( ) ( ) Subset of ) :] : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) & S : ( ( Function-like V18([:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) ) ( Relation-like [:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) -valued Function-like V18([:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) V119() V120() V121() ) Function of [:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) = the scalar of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( Function-like V18([: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) V119() V120() V121() ) Element of bool [:[: the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) :] : ( ( ) ( non empty V119() V120() V121() ) set ) : ( ( ) ( non empty ) set ) ) || V1 : ( ( ) ( ) Subset of ) : ( ( ) ( Relation-like Function-like ) set ) holds
UNITSTR(# 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() V129() V130() V131() V135() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) 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() V129() V130() V131() V135() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) Function of [:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ,S : ( ( Function-like V18([:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) ) ( Relation-like [:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) -valued Function-like V18([:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) V119() V120() V121() ) Function of [:b3 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) #) : ( ( strict ) ( non empty strict ) UNITSTR ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:19
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) holds V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:20
for V, X being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) st V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) & X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) holds
V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) = X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ;

theorem :: RUSUB_1:21
for V, X, Y being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) st V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & X : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds
V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of Y : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:22
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2 being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st the carrier of W1 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) c= the carrier of W2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) holds
W1 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:23
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2 being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st ( for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W1 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds
v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
W1 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

registration
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ;
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like for ( ( ) ( ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) ;
end;

theorem :: RUSUB_1:24
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2 being ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st the carrier of W1 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) = the carrier of W2 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) holds
W1 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = W2 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:25
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2 being ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st ( for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W1 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) iff v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W2 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ) holds
W1 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = W2 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:26
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) st the carrier of W : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) = the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) holds
W : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) = V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ;

theorem :: RUSUB_1:27
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) st ( for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) iff v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
W : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) = V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ;

theorem :: RUSUB_1:28
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for V1 being ( ( ) ( ) Subset of ) st the carrier of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) = V1 : ( ( ) ( ) Subset of ) holds
V1 : ( ( ) ( ) Subset of ) is linearly-closed ;

theorem :: RUSUB_1:29
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for V1 being ( ( ) ( ) Subset of ) st V1 : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( Function-like functional empty V129() V130() V131() V132() V133() V134() V135() ) set ) & V1 : ( ( ) ( ) Subset of ) is linearly-closed holds
ex W being ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st V1 : ( ( ) ( ) Subset of ) = the carrier of W : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ;

begin

definition
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ;
func (0). V -> ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) means :: RUSUB_1:def 2
 the carrier of it : ( ( ) ( ) Element of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( ) set ) = {(0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( V55(V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) right_complementable ) Element of the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ;
func (Omega). V -> ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) equals :: RUSUB_1:def 3
 UNITSTR(# the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) , the ZeroF of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( right_complementable ) Element of the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) ) , the addF of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( Function-like V18([: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , the scalar of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( Function-like V18([: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) ) ( Relation-like [: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) ) V119() V120() V121() ) Element of bool [:[: the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) :] : ( ( ) ( non empty V119() V120() V121() ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) UNITSTR ) ;
end;

begin

theorem :: RUSUB_1:30
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds (0). W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) = (0). V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:31
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2 being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds (0). W1 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) = (0). W2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b3 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:32
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds (0). W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:33
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds (0). V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:34
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2 being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds (0). W1 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:35
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) holds V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) is ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of (Omega). V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

begin

definition
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ;
let v be ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ;
let W be ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;
func v + W -> ( ( ) ( ) Subset of ) equals :: RUSUB_1:def 4
 { (v : ( ( ) ( ) Element of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) + u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) : ( ( ) ( non empty ) set ) ) where u is ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : u : ( ( ) ( right_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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) ) ( Relation-like [:V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( ) set ) -defined V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) -valued Function-like V18([:V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) ) Element of bool [:[:V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( ) 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ;
let W be ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;
mode Coset of W -> ( ( ) ( ) Subset of ) means :: RUSUB_1:def 5
 ex v being ( ( ) ( right_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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) ) ( Relation-like [:V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( ) set ) -defined V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) -valued Function-like V18([:V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) ) Element of bool [:[:V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) UNITSTR ) ) : ( ( ) ( ) Subset of ) ;
end;

begin

theorem :: RUSUB_1:36
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( 0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( V55(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) iff v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:37
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) ;

theorem :: RUSUB_1:38
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds (0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( V55(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = the carrier of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ;

theorem :: RUSUB_1:39
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds v : ( ( ) ( right_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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = {v : ( ( ) ( right_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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_1:40
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds v : ( ( ) ( right_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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ;

theorem :: RUSUB_1:41
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( 0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( V55(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) iff v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = the carrier of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_1:42
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) iff v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = the carrier of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_1:43
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( ext-real V34() real ) Real) st v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds
(a : ( ( ) ( ext-real V34() real ) Real) * v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = the carrier of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ;

theorem :: RUSUB_1:44
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( ext-real V34() real ) Real) st a : ( ( ) ( ext-real V34() real ) Real) <> 0 : ( ( ) ( Function-like functional empty ext-real natural V34() real V117() V118() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of bool REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) : ( ( ) ( non empty ) set ) ) ) & (a : ( ( ) ( ext-real V34() real ) Real) * v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = the carrier of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) holds
v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:45
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) iff (- v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = the carrier of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_1:46
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) iff v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = (v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) ) ;

theorem :: RUSUB_1:47
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) iff v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = (v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) ) ;

theorem :: RUSUB_1:48
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) iff u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) ) ;

theorem :: RUSUB_1:49
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = (- v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) iff v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:50
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v1, v2 being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) & u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v2 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) holds
v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = v2 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) ;

theorem :: RUSUB_1:51
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) & u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in (- v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) holds
v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:52
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( ext-real V34() real ) Real) st a : ( ( ) ( ext-real V34() real ) Real) <> 1 : ( ( ) ( non empty ext-real natural V34() real V117() V118() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of bool REAL : ( ( ) ( non empty V36() V129() V130() V131() V135() ) set ) : ( ( ) ( non empty ) set ) ) ) & a : ( ( ) ( ext-real V34() real ) Real) * v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) holds
v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:53
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( ext-real V34() real ) Real) st v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds
a : ( ( ) ( ext-real V34() real ) Real) * v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) ;

theorem :: RUSUB_1:54
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( - v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) iff v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:55
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) iff u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:56
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) iff u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:57
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) iff ex v1 being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st
( v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: RUSUB_1:58
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) iff ex v1 being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st
( v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: RUSUB_1:59
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v1, v2 being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( ex v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st
( v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) & v2 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) ) iff v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - v2 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:60
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) holds
ex v1 being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st
( v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) = u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_1:61
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) holds
ex v1 being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st
( v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) = u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_1:62
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2 being ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W1 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W2 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) iff W1 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = W2 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:63
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2 being ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W1 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) = u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W2 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) holds
W1 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = W2 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:64
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for C being ( ( ) ( ) Coset of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
( C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) is linearly-closed iff C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) = the carrier of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_1:65
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2 being ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for C1 being ( ( ) ( ) Coset of W1 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) )
for C2 being ( ( ) ( ) Coset of W2 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) st C1 : ( ( ) ( ) Coset of b2 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) = C2 : ( ( ) ( ) Coset of b3 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
W1 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = W2 : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_1:66
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds {v : ( ( ) ( right_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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:67
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
ex v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st V1 : ( ( ) ( ) Subset of ) = {v : ( ( ) ( right_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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_1:68
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds the carrier of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) is ( ( ) ( ) Coset of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:69
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) holds the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:70
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) 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 RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ;

theorem :: RUSUB_1:71
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for C being ( ( ) ( ) Coset of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
( 0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( V55(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) iff C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) = the carrier of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_1:72
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for C being ( ( ) ( ) Coset of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) )
for u being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) iff C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) = u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Subset of ) ) ;

theorem :: RUSUB_1:73
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for C being ( ( ) ( ) Coset of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) & v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
ex v1 being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st
( v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) + v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_1:74
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for C being ( ( ) ( ) Coset of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) )
for u, v being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) & v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
ex v1 being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) st
( v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_1:75
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v1, v2 being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( ex C being ( ( ) ( ) Coset of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) st
( v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) & v2 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ) iff v1 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) - v2 : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) in W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_1:76
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for u being ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) )
for B, C being ( ( ) ( ) Coset of W : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) st u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in B : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) & u : ( ( ) ( right_complementable ) VECTOR of ( ( ) ( non empty ) set ) ) in C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
B : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) = C : ( ( ) ( ) Coset of b2 : ( ( ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;