:: RLVECT_3 semantic presentation

begin

theorem :: RLVECT_3:1
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for L1, L2 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) holds Sum (L1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) + L2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = (Sum L1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + (Sum L2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_3:2
for a being ( ( ) ( V22() V23() V24() ) Real)
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for L being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) holds Sum (a : ( ( ) ( V22() V23() V24() ) Real) * L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = a : ( ( ) ( V22() V23() V24() ) Real) * (Sum L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_3:3
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) holds Sum (- L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_3:4
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for L1, L2 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) holds Sum (L1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) - L2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = (Sum L1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) - (Sum L2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

definition
let V be ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ;
let A be ( ( ) ( ) Subset of ) ;
attr A is linearly-independent means :: RLVECT_3:def 1
 for l being ( ( ) ( Relation-like the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of A : ( ( ) ( ) Element of V : ( ( ) ( ) RLSStruct ) ) ) st Sum l : ( ( ) ( Relation-like the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) ) = 0. V : ( ( ) ( ) RLSStruct ) : ( ( ) ( V55(V : ( ( ) ( ) RLSStruct ) ) ) Element of the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) ) holds
Carrier l : ( ( ) ( Relation-like the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of A : ( ( ) ( ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of V : ( ( ) ( ) RLSStruct ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() ) set ) ;
end;

notation
let V be ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ;
let A be ( ( ) ( ) Subset of ) ;
antonym linearly-dependent A for linearly-independent ;
end;

theorem :: RLVECT_3:5
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) & B : ( ( ) ( ) Subset of ) is linearly-independent holds
A : ( ( ) ( ) Subset of ) is linearly-independent ;

theorem :: RLVECT_3:6
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is linearly-independent holds
not 0. V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( V55(b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) ;

theorem :: RLVECT_3:7
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) holds {} the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is linearly-independent ;

registration
let V be ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ;
cluster linearly-independent for ( ( ) ( ) Element of bool the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: RLVECT_3:8
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( {v : ( ( ) ( ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is linearly-independent iff v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> 0. V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( V55(b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLVECT_3:9
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) holds {(0. V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( ) ( V55(b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is linearly-dependent ;

theorem :: RLVECT_3:10
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for v1, v2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st {v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is linearly-independent holds
( v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> 0. V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( V55(b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) & v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> 0. V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( V55(b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLVECT_3:11
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( {v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,(0. V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( ) ( V55(b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is linearly-dependent & {(0. V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( ) ( V55(b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is linearly-dependent ) ;

theorem :: RLVECT_3:12
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for v1, v2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & {v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is linearly-independent iff ( v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> 0. V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( V55(b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) & ( for a being ( ( ) ( V22() V23() V24() ) Real) holds v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> a : ( ( ) ( V22() V23() V24() ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ) ) ;

theorem :: RLVECT_3:13
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for v1, v2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( ( v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) <> v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) & {v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is linearly-independent ) iff for a, b being ( ( ) ( V22() V23() V24() ) Real) st (a : ( ( ) ( V22() V23() V24() ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + (b : ( ( ) ( V22() V23() V24() ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = 0. V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( V55(b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( V22() V23() V24() ) Real) = 0 : ( ( ) ( Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty non trivial non finite ) set ) : ( ( ) ( non empty ) set ) ) ) & b : ( ( ) ( V22() V23() V24() ) Real) = 0 : ( ( ) ( Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty non trivial non finite ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) ;

definition
let V be ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ;
let A be ( ( ) ( ) Subset of ) ;
func Lin A -> ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) ) means :: RLVECT_3:def 2
 the carrier of it : ( ( Function-like quasi_total ) ( Relation-like [:V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) ,V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) :] : ( ( ) ( ) set ) -defined V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) -valued Function-like quasi_total ) Element of bool [:[:V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) ,V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) :] : ( ( ) ( ) set ) ,V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) :] : ( ( ) ( ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of A : ( ( ) ( ) Subset of ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) where l is ( ( ) ( Relation-like the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of A : ( ( ) ( ) Element of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) ) ) : verum } ;
end;

theorem :: RLVECT_3:14
for x being ( ( ) ( ) set )
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) holds
( x : ( ( ) ( ) set ) in Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) iff ex l being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of A : ( ( ) ( ) Subset of ) ) st x : ( ( ) ( ) set ) = Sum l : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Linear_Combination of b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLVECT_3:15
for x being ( ( ) ( ) set )
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) st x : ( ( ) ( ) set ) in A : ( ( ) ( ) Subset of ) holds
x : ( ( ) ( ) set ) in Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ;

theorem :: RLVECT_3:16
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) holds Lin ({} the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() ) Element of bool the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) = (0). V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ;

theorem :: RLVECT_3:17
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) holds
( not Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) = (0). V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) or A : ( ( ) ( ) Subset of ) = {} : ( ( ) ( Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() ) set ) or A : ( ( ) ( ) Subset of ) = {(0. V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( ) ( V55(b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLVECT_3:18
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of )
for W being ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) st A : ( ( ) ( ) Subset of ) = the carrier of W : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( ) ( non empty ) set ) holds
Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) = W : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ;

theorem :: RLVECT_3:19
for V being ( ( non empty V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = the carrier of V : ( ( non empty V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) holds
Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) = V : ( ( non empty V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ;

theorem :: RLVECT_3:20
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) holds
Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) is ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of Lin B : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) ;

theorem :: RLVECT_3:21
for V being ( ( non empty V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for A, B being ( ( ) ( ) Subset of ) st Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) = V : ( ( non empty V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) & A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) holds
Lin B : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) = V : ( ( non empty V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ;

theorem :: RLVECT_3:22
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) = (Lin A : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) + (Lin B : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ;

theorem :: RLVECT_3:23
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) is ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of (Lin A : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) /\ (Lin B : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) ;

theorem :: RLVECT_3:24
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
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 V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) = RLSStruct(# the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the ZeroF of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) , the U5 of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( Function-like quasi_total ) ( Relation-like [:REAL : ( ( ) ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of bool [:[:REAL : ( ( ) ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) ) ;

theorem :: RLVECT_3:25
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) st Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) = V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) 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 V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) = V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ;

definition
let V be ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ;
mode Basis of V -> ( ( ) ( ) Subset of ) means :: RLVECT_3:def 3
( it : ( ( ) ( ) Element of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) ) is linearly-independent & Lin it : ( ( ) ( ) Element of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) ) = RLSStruct(# the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) , the ZeroF of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( ) Element of the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) , the U5 of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of bool [:[: the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , the Mult of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( Function-like quasi_total ) ( Relation-like [:REAL : ( ( ) ( non empty non trivial non finite ) set ) , the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty non trivial non finite ) set ) , the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RLSStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) );
end;

theorem :: RLVECT_3:26
for V being ( ( non empty V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is linearly-independent holds
ex I being ( ( ) ( ) Basis of V : ( ( non empty V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) st A : ( ( ) ( ) Subset of ) c= I : ( ( ) ( ) Basis of b1 : ( ( non empty V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ;

theorem :: RLVECT_3:27
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) st Lin A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) = V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) holds
ex I being ( ( ) ( ) Basis of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) st I : ( ( ) ( ) Basis of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) c= A : ( ( ) ( ) Subset of ) ;

theorem :: RLVECT_3:28
for M being ( ( non empty ) ( non empty ) set )
for CF being ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined union b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Choice_Function of M : ( ( non empty ) ( non empty ) set ) ) st not {} : ( ( ) ( Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() ) set ) in M : ( ( non empty ) ( non empty ) set ) holds
dom CF : ( ( ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined union b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Choice_Function of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) = M : ( ( non empty ) ( non empty ) set ) ;

theorem :: RLVECT_3:29
for x being ( ( ) ( ) set )
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) holds
( x : ( ( ) ( ) set ) in (0). V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) iff x : ( ( ) ( ) set ) = 0. V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( V55(b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) Element of the carrier of b2 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLVECT_3:30
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for W1, W3, W2 being ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) st W1 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) is ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W3 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) holds
W1 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) /\ W2 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) is ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W3 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) ;

theorem :: RLVECT_3:31
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for W1, W2, W3 being ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) st W1 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) is ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W2 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) & W1 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) is ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W3 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) holds
W1 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) is ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W2 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) /\ W3 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) ;

theorem :: RLVECT_3:32
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for W1, W3, W2 being ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) st W1 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) is ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W3 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) & W2 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) is ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W3 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) holds
W1 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) + W2 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) is ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W3 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) ;

theorem :: RLVECT_3:33
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for W1, W2, W3 being ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) st W1 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) is ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W2 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) holds
W1 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) is ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of W2 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) + W3 : ( ( ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) : ( ( strict ) ( non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) Subspace of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) ) ) ;

theorem :: RLVECT_3:34
for V being ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace)
for F, G being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty non trivial non finite ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) )
for f being ( ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Function of the carrier of V : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) holds f : ( ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Function of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) (#) (F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty non trivial non finite ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ^ G : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty non trivial non finite ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty non trivial non finite ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty non trivial non finite ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = (f : ( ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Function of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) (#) F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty non trivial non finite ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty non trivial non finite ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ^ (f : ( ( 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite ) set ) -valued Function-like quasi_total ) Function of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite ) set ) ) (#) G : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty non trivial non finite ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty non trivial non finite ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( non empty non trivial non finite ) 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 ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of the carrier of b1 : ( ( non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;