:: RUSUB_3 semantic presentation

begin

definition
let V be ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ;
let A be ( ( ) ( ) Subset of ) ;
func Lin A -> ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of V : ( ( ) ( ) UNITSTR ) ) means :: RUSUB_3:def 1
 the carrier of it : ( ( Function-like quasi_total ) ( Relation-like [:V : ( ( ) ( ) UNITSTR ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) ( ) set ) -defined V : ( ( ) ( ) UNITSTR ) -valued Function-like quasi_total ) Element of bool [:[:V : ( ( ) ( ) UNITSTR ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) ( ) set ) ,V : ( ( ) ( ) UNITSTR ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = { (Sum l : ( ( ) ( Relation-like the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of A : ( ( ) ( ) Subset of ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) ) where l is ( ( ) ( Relation-like the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of A : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) ) : verum } ;
end;

theorem :: RUSUB_3:1
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for A being ( ( ) ( ) Subset of )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) iff ex l being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of A : ( ( ) ( ) Subset of ) ) st x : ( ( ) ( ) set ) = Sum l : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b2 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_3:2
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for A being ( ( ) ( ) Subset of )
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in A : ( ( ) ( ) Subset of ) holds
x : ( ( ) ( ) set ) in Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_3:3
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) holds Lin ({} the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V40() cardinal {} : ( ( ) ( ) set ) -element FinSequence-membered V120() V121() V122() V123() V124() V125() V126() ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = (0). V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_3:4
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for A being ( ( ) ( ) Subset of ) holds
( not Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = (0). V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) or A : ( ( ) ( ) Subset of ) = {} : ( ( ) ( ) set ) or A : ( ( ) ( ) Subset of ) = {(0. V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( V55(b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_3:5
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = the carrier of W : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) holds
Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = W : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_3:6
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) holds
Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) = V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ;

theorem :: RUSUB_3:7
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) holds
Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of Lin B : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_3:8
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace)
for A, B being ( ( ) ( ) Subset of ) st Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) = V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) & A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) holds
Lin B : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) = V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ;

theorem :: RUSUB_3:9
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for A, B being ( ( ) ( ) Subset of ) holds Lin (A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = (Lin A : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) + (Lin B : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_3:10
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for A, B being ( ( ) ( ) Subset of ) holds Lin (A : ( ( ) ( ) Subset of ) /\ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of (Lin A : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) /\ (Lin B : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_3:11
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is linearly-independent holds
ex B being ( ( ) ( ) Subset of ) st
( A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) & B : ( ( ) ( ) Subset of ) is linearly-independent & Lin B : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = UNITSTR(# the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) , the ZeroF of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) , the U5 of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() 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 V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() 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 V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [:[: the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() 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 V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() 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 V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() 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 ) ) , the Mult of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( Function-like quasi_total ) ( Relation-like [:REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) , the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty non trivial non finite ) set ) -defined the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) , the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty non trivial non finite ) set ) , the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty non trivial non finite ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) , the scalar of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() 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 V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() 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 non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like non empty total quasi_total ) Element of bool [:[: the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() 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 V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() 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 non trivial non finite V120() V121() V122() V126() ) set ) :] : ( ( ) ( non empty non trivial non finite ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) #) : ( ( strict ) ( non empty strict ) UNITSTR ) ) ;

theorem :: RUSUB_3:12
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for A being ( ( ) ( ) Subset of ) st Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) holds
ex B being ( ( ) ( ) Subset of ) st
( B : ( ( ) ( ) Subset of ) c= A : ( ( ) ( ) Subset of ) & B : ( ( ) ( ) Subset of ) is linearly-independent & Lin B : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

begin

definition
let V be ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ;
mode Basis of V -> ( ( ) ( ) Subset of ) means :: RUSUB_3:def 2
( it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) is linearly-independent & Lin it : ( ( ) ( ) Element of V : ( ( ) ( ) UNITSTR ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of V : ( ( ) ( ) UNITSTR ) ) = UNITSTR(# the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) , the ZeroF of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) ) , the U5 of V : ( ( ) ( ) UNITSTR ) : ( ( Function-like quasi_total ) ( 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 quasi_total ) 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 Mult of V : ( ( ) ( ) UNITSTR ) : ( ( Function-like quasi_total ) ( Relation-like [:REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the scalar of V : ( ( ) ( ) UNITSTR ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Element of bool [:[: the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) UNITSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) UNITSTR ) );
end;

theorem :: RUSUB_3:13
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is linearly-independent holds
ex I being ( ( ) ( ) Basis of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) st A : ( ( ) ( ) Subset of ) c= I : ( ( ) ( ) Basis of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_3:14
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for A being ( ( ) ( ) Subset of ) st Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) holds
ex I being ( ( ) ( ) Basis of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st I : ( ( ) ( ) Basis of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) c= A : ( ( ) ( ) Subset of ) ;

theorem :: RUSUB_3:15
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is linearly-independent holds
ex I being ( ( ) ( ) Basis of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st A : ( ( ) ( ) Subset of ) c= I : ( ( ) ( ) Basis of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

begin

theorem :: RUSUB_3:16
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for L being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for A being ( ( ) ( ) Subset of )
for F being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) st rng F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( finite ) set ) c= the carrier of (Lin A : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) holds
ex K being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of A : ( ( ) ( ) Subset of ) ) st Sum (L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) (#) F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) = Sum K : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_3:17
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for L being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for A being ( ( ) ( ) Subset of ) st Carrier L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= the carrier of (Lin A : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) holds
ex K being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of A : ( ( ) ( ) Subset of ) ) st Sum L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) = Sum K : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RUSUB_3:18
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for L being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st Carrier L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= the carrier of W : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) holds
for K being ( ( ) ( Relation-like the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of W : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) st K : ( ( ) ( Relation-like the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) = L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) | the carrier of W : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like ) Element of bool [: the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) :] : ( ( ) ( non empty non trivial non finite ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) holds
( Carrier L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = Carrier K : ( ( ) ( Relation-like the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) : ( ( ) ( finite ) Element of bool the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & Sum L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) = Sum K : ( ( ) ( Relation-like the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_3:19
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for K being ( ( ) ( Relation-like the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of W : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ex L being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st
( Carrier K : ( ( ) ( Relation-like the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) : ( ( ) ( finite ) Element of bool the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = Carrier L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & Sum K : ( ( ) ( Relation-like the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) = Sum L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_3:20
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for L being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st Carrier L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= the carrier of W : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) holds
ex K being ( ( ) ( Relation-like the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of W : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) st
( Carrier K : ( ( ) ( Relation-like the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) : ( ( ) ( finite ) Element of bool the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = Carrier L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & Sum K : ( ( ) ( Relation-like the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) ) = Sum L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_3:21
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for I being ( ( ) ( ) Basis of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin I : ( ( ) ( ) Basis of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_3:22
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is linearly-independent holds
A : ( ( ) ( ) Subset of ) is ( ( linearly-independent ) ( linearly-independent ) Subset of ) ;

theorem :: RUSUB_3:23
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is linearly-independent & A : ( ( ) ( ) Subset of ) c= the carrier of W : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) holds
A : ( ( ) ( ) Subset of ) is ( ( linearly-independent ) ( linearly-independent ) Subset of ) ;

theorem :: RUSUB_3:24
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for A being ( ( ) ( ) Basis of W : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ex B being ( ( ) ( ) Basis of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st A : ( ( ) ( ) Basis of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) c= B : ( ( ) ( ) Basis of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_3:25
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is linearly-independent holds
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) holds
for B being ( ( ) ( ) Subset of ) st B : ( ( ) ( ) Subset of ) = A : ( ( ) ( ) Subset of ) \ {v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
not v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin B : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_3:26
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for I being ( ( ) ( ) Basis of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for A being ( ( non empty ) ( non empty ) Subset of ) st A : ( ( non empty ) ( non empty ) Subset of ) misses I : ( ( ) ( ) Basis of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds
for B being ( ( ) ( ) Subset of ) st B : ( ( ) ( ) Subset of ) = I : ( ( ) ( ) Basis of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) \/ A : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
B : ( ( ) ( ) Subset of ) is linearly-dependent ;

theorem :: RUSUB_3:27
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= the carrier of W : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( non empty ) set ) holds
Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_3:28
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W being ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for A being ( ( ) ( ) Subset of )
for B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = B : ( ( ) ( ) Subset of ) holds
Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = Lin B : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

begin

theorem :: RUSUB_3:29
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in Lin {v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) iff ex a being ( ( ) ( ext-real V25() V26() ) Real) st x : ( ( ) ( ) set ) = a : ( ( ) ( ext-real V25() V26() ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_3:30
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_3:31
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for v, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (Lin {w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) iff ex a being ( ( ) ( ext-real V25() V26() ) Real) st x : ( ( ) ( ) set ) = v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (a : ( ( ) ( ext-real V25() V26() ) Real) * w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_3:32
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for w1, w2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) iff ex a, b being ( ( ) ( ext-real V25() V26() ) Real) st x : ( ( ) ( ) set ) = (a : ( ( ) ( ext-real V25() V26() ) Real) * w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) + (b : ( ( ) ( ext-real V25() V26() ) Real) * w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_3:33
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for w1, w2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_3:34
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for v, w1, w2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) iff ex a, b being ( ( ) ( ext-real V25() V26() ) Real) st x : ( ( ) ( ) set ) = (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (a : ( ( ) ( ext-real V25() V26() ) Real) * w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) + (b : ( ( ) ( ext-real V25() V26() ) Real) * w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_3:35
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for v1, v2, v3 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in Lin {v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) iff ex a, b, c being ( ( ) ( ext-real V25() V26() ) Real) st x : ( ( ) ( ) set ) = ((a : ( ( ) ( ext-real V25() V26() ) Real) * v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) + (b : ( ( ) ( ext-real V25() V26() ) Real) * v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) + (c : ( ( ) ( ext-real V25() V26() ) Real) * v3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_3:36
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for w1, w2, w3 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & w3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_3:37
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for v, w1, w2, w3 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) iff ex a, b, c being ( ( ) ( ext-real V25() V26() ) Real) st x : ( ( ) ( ) set ) = ((v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (a : ( ( ) ( ext-real V25() V26() ) Real) * w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) + (b : ( ( ) ( ext-real V25() V26() ) Real) * w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) + (c : ( ( ) ( ext-real V25() V26() ) Real) * w3 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_3:38
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for v, w being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> 0. V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( V55(b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) holds
Lin {v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = Lin {w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V120() V121() V122() V126() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ;

theorem :: RUSUB_3:39
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for v1, v2, w1, w2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & {v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is linearly-independent & v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) holds
( Lin {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) = Lin {v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) & {w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( finite ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is linearly-independent & w1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> w2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

begin

theorem :: RUSUB_3:40
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in (0). V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) iff x : ( ( ) ( ) set ) = 0. V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( V55(b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RUSUB_3:41
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2, W3 being ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st W1 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W3 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
W1 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) /\ W2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W3 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_3:42
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2, W3 being ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st W1 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) & W1 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W3 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
W1 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) /\ W3 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_3:43
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2, W3 being ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st W1 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W3 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) & W2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W3 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
W1 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) + W2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W3 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_3:44
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2, W3 being ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) st W1 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
W1 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) + W3 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( strict ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) ;

theorem :: RUSUB_3:45
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace)
for W1, W2 being ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) )
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st W1 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) is ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of W2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) ) holds
v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + W1 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + W2 : ( ( ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like ) RealUnitarySpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;