:: RLAFFIN1 semantic presentation

begin

registration
let RLS be ( ( non empty ) ( non empty ) RLSStruct ) ;
let A be ( ( empty ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty non trivial non finite V65() V66() V67() V68() V71() ) set ) -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} : ( ( ) ( ) set ) -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() ) Subset of ) ;
cluster conv A : ( ( empty ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty non trivial non finite V65() V66() V67() V68() V71() ) set ) -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} : ( ( ) ( ) set ) -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() ) Element of K19( the carrier of RLS : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( convex ) ( convex ) Element of K19( the carrier of RLS : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -> empty convex ;
end;

registration
let RLS be ( ( non empty ) ( non empty ) RLSStruct ) ;
let A be ( ( non empty ) ( non empty ) Subset of ) ;
cluster conv A : ( ( non empty ) ( non empty ) Element of K19( the carrier of RLS : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( convex ) ( convex ) Element of K19( the carrier of RLS : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -> non empty convex ;
end;

theorem :: RLAFFIN1:1
for R being ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct )
for v being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds conv {v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of K19( the carrier of b1 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( convex ) ( non empty convex ) Element of K19( the carrier of b1 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = {v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of K19( the carrier of b1 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:2
for RLS being ( ( non empty ) ( non empty ) RLSStruct )
for A being ( ( ) ( ) Subset of ) holds A : ( ( ) ( ) Subset of ) c= conv A : ( ( ) ( ) Subset of ) : ( ( convex ) ( convex ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:3
for RLS being ( ( non empty ) ( non empty ) RLSStruct )
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) holds
conv A : ( ( ) ( ) Subset of ) : ( ( convex ) ( convex ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= conv B : ( ( ) ( ) Subset of ) : ( ( convex ) ( convex ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:4
for RLS being ( ( non empty ) ( non empty ) RLSStruct )
for S, A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= conv S : ( ( ) ( ) Subset of ) : ( ( convex ) ( convex ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
conv S : ( ( ) ( ) Subset of ) : ( ( convex ) ( convex ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = conv (S : ( ( ) ( ) Subset of ) \/ A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( convex ) ( convex ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:5
for V being ( ( non empty add-associative ) ( non empty add-associative ) addLoopStr )
for A being ( ( ) ( ) Subset of )
for v, w being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty add-associative ) ( non empty add-associative ) addLoopStr ) : ( ( ) ( non empty ) set ) ) + A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty add-associative ) ( non empty add-associative ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty add-associative ) ( non empty add-associative ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty add-associative ) ( non empty add-associative ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:6
for V being ( ( non empty Abelian right_zeroed ) ( non empty Abelian right_zeroed V135() ) addLoopStr )
for A being ( ( ) ( ) Subset of ) holds (0. V : ( ( non empty Abelian right_zeroed ) ( non empty Abelian right_zeroed V135() ) addLoopStr ) ) : ( ( ) ( V84(b1 : ( ( non empty Abelian right_zeroed ) ( non empty Abelian right_zeroed V135() ) addLoopStr ) ) ) Element of the carrier of b1 : ( ( non empty Abelian right_zeroed ) ( non empty Abelian right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) + A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty Abelian right_zeroed ) ( non empty Abelian right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = A : ( ( ) ( ) Subset of ) ;

theorem :: RLAFFIN1:7
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr )
for g being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) holds card A : ( ( ) ( ) Subset of ) : ( ( cardinal ) ( ordinal cardinal ) set ) = card (g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( cardinal ) ( ordinal cardinal ) set ) ;

theorem :: RLAFFIN1:8
for S being ( ( non empty ) ( non empty ) addLoopStr )
for v being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + ({} S : ( ( non empty ) ( non empty ) addLoopStr ) ) : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty non trivial non finite V65() V66() V67() V68() V71() ) set ) -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} : ( ( ) ( ) set ) -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = {} S : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty non trivial non finite V65() V66() V67() V68() V71() ) set ) -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} : ( ( ) ( ) set ) -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:9
for r being ( ( ) ( V24() V32() ext-real ) Real)
for RLS being ( ( non empty ) ( non empty ) RLSStruct )
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) holds
r : ( ( ) ( V24() V32() ext-real ) Real) * A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= r : ( ( ) ( V24() V32() ext-real ) Real) * B : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:10
for r, s being ( ( ) ( V24() V32() ext-real ) Real)
for R being ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct )
for AR being ( ( ) ( ) Subset of ) holds (r : ( ( ) ( V24() V32() ext-real ) Real) * s : ( ( ) ( V24() V32() ext-real ) Real) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) * AR : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b3 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = r : ( ( ) ( V24() V32() ext-real ) Real) * (s : ( ( ) ( V24() V32() ext-real ) Real) * AR : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b3 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b3 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:11
for R being ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct )
for AR being ( ( ) ( ) Subset of ) holds 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) * AR : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = AR : ( ( ) ( ) Subset of ) ;

theorem :: RLAFFIN1:12
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) holds 0 : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) * A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= {(0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) : ( ( ) ( V84(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:13
for S being ( ( non empty ) ( non empty ) addLoopStr )
for LS1, LS2 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of S : ( ( non empty ) ( non empty ) addLoopStr ) )
for F being ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) holds (LS1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) + LS2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) * F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like FinSequence-like V55() V56() V57() ) FinSequence of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) = (LS1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) * F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like FinSequence-like V55() V56() V57() ) FinSequence of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) + (LS2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) * F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like FinSequence-like V55() V56() V57() ) FinSequence of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like FinSequence-like V55() V56() V57() ) FinSequence of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) ;

theorem :: RLAFFIN1:14
for r being ( ( ) ( V24() V32() ext-real ) Real)
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for L being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) )
for F being ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) holds (r : ( ( ) ( V24() V32() ext-real ) Real) * L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) * F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like FinSequence-like V55() V56() V57() ) FinSequence of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) = r : ( ( ) ( V24() V32() ext-real ) Real) * (L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) * F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like FinSequence-like V55() V56() V57() ) FinSequence of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like FinSequence-like V55() V56() V57() ) FinSequence of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) ;

theorem :: RLAFFIN1:15
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is linearly-independent & A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) & Lin B : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) = V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) holds
ex I being ( ( linearly-independent ) ( linearly-independent ) Subset of ) st
( A : ( ( ) ( ) Subset of ) c= I : ( ( linearly-independent ) ( linearly-independent ) Subset of ) & I : ( ( linearly-independent ) ( linearly-independent ) Subset of ) c= B : ( ( ) ( ) Subset of ) & Lin I : ( ( linearly-independent ) ( linearly-independent ) Subset of ) : ( ( strict ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) = V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ;

begin

definition
let G be ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ;
let LG be ( ( ) ( Relation-like the carrier of G : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of G : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) ;
let g be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func g + LG -> ( ( ) ( Relation-like the carrier of G : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of G : ( ( ) ( ) set ) ) means :: RLAFFIN1:def 1
for h being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds it : ( ( Function-like quasi_total ) ( Relation-like K20(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ,G : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) -defined G : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of K19(K20(K20(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ,G : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ,G : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) . h : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) = LG : ( ( ) ( ) set ) . (h : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) - g : ( ( Function-like quasi_total ) ( Relation-like K20(G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) -defined G : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of K19(K20(K20(G : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ,G : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of G : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) ;
end;

theorem :: RLAFFIN1:16
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr )
for LG being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of G : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) )
for g being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds Carrier (g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + LG : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) : ( ( ) ( finite ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (Carrier LG : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) ) : ( ( ) ( finite ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:17
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr )
for LG1, LG2 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of G : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) )
for g being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (LG1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) + LG2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) = (g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + LG1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) + (g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + LG2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) ;

theorem :: RLAFFIN1:18
for r being ( ( ) ( V24() V32() ext-real ) Real)
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for L being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) holds v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (r : ( ( ) ( V24() V32() ext-real ) Real) * L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) = r : ( ( ) ( V24() V32() ext-real ) Real) * (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ;

theorem :: RLAFFIN1:19
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr )
for LG being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of G : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) )
for g, h being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (h : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + LG : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) = (g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + h : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) + LG : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) ;

theorem :: RLAFFIN1:20
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr )
for g being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (ZeroLC G : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) = ZeroLC G : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) ;

theorem :: RLAFFIN1:21
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr )
for LG being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of G : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) holds (0. G : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) : ( ( ) ( V84(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) + LG : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) = LG : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) ;

definition
let R be ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ;
let LR be ( ( ) ( Relation-like the carrier of R : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of R : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ;
let r be ( ( ) ( V24() V32() ext-real ) Real) ;
func r (*) LR -> ( ( ) ( Relation-like the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of R : ( ( ) ( ) set ) ) means :: RLAFFIN1:def 2
for v being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds it : ( ( Function-like quasi_total ) ( Relation-like K20(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) -defined R : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of K19(K20(K20(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) . v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) = LR : ( ( ) ( ) set ) . ((r : ( ( Function-like quasi_total ) ( Relation-like K20(R : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) -defined R : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of K19(K20(K20(R : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ") : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) * v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) if r : ( ( Function-like quasi_total ) ( Relation-like K20(R : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) -defined R : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of K19(K20(K20(R : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) <> 0 : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) )
otherwise it : ( ( Function-like quasi_total ) ( Relation-like K20(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) -defined R : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of K19(K20(K20(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) = ZeroLC R : ( ( ) ( ) set ) : ( ( ) ( Relation-like the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of R : ( ( ) ( ) set ) ) ;
end;

theorem :: RLAFFIN1:22
for r being ( ( ) ( V24() V32() ext-real ) Real)
for R being ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct )
for LR being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of R : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) holds Carrier (r : ( ( ) ( V24() V32() ext-real ) Real) (*) LR : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) : ( ( ) ( finite ) Element of K19( the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= r : ( ( ) ( V24() V32() ext-real ) Real) * (Carrier LR : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ) : ( ( ) ( finite ) Element of K19( the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:23
for r being ( ( ) ( V24() V32() ext-real ) Real)
for R being ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct )
for LR being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of R : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) st r : ( ( ) ( V24() V32() ext-real ) Real) <> 0 : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
Carrier (r : ( ( ) ( V24() V32() ext-real ) Real) (*) LR : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) : ( ( ) ( finite ) Element of K19( the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = r : ( ( ) ( V24() V32() ext-real ) Real) * (Carrier LR : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ) : ( ( ) ( finite ) Element of K19( the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:24
for r being ( ( ) ( V24() V32() ext-real ) Real)
for R being ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct )
for LR1, LR2 being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of R : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) holds r : ( ( ) ( V24() V32() ext-real ) Real) (*) (LR1 : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) + LR2 : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) = (r : ( ( ) ( V24() V32() ext-real ) Real) (*) LR1 : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) + (r : ( ( ) ( V24() V32() ext-real ) Real) (*) LR2 : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ;

theorem :: RLAFFIN1:25
for r, s being ( ( ) ( V24() V32() ext-real ) Real)
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for L being ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) holds r : ( ( ) ( V24() V32() ext-real ) Real) * (s : ( ( ) ( V24() V32() ext-real ) Real) (*) L : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) = s : ( ( ) ( V24() V32() ext-real ) Real) (*) (r : ( ( ) ( V24() V32() ext-real ) Real) * L : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ;

theorem :: RLAFFIN1:26
for r being ( ( ) ( V24() V32() ext-real ) Real)
for R being ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) holds r : ( ( ) ( V24() V32() ext-real ) Real) (*) (ZeroLC R : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) = ZeroLC R : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ;

theorem :: RLAFFIN1:27
for r, s being ( ( ) ( V24() V32() ext-real ) Real)
for R being ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct )
for LR being ( ( ) ( Relation-like the carrier of b3 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of R : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) holds r : ( ( ) ( V24() V32() ext-real ) Real) (*) (s : ( ( ) ( V24() V32() ext-real ) Real) (*) LR : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ) : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) = (r : ( ( ) ( V24() V32() ext-real ) Real) * s : ( ( ) ( V24() V32() ext-real ) Real) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) (*) LR : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ;

theorem :: RLAFFIN1:28
for R being ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct )
for LR being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of R : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) holds 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) (*) LR : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) = LR : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ;

begin

definition
let S be ( ( non empty ) ( non empty ) addLoopStr ) ;
let LS be ( ( ) ( Relation-like the carrier of S : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of S : ( ( non empty ) ( non empty ) addLoopStr ) ) ;
func sum LS -> ( ( ) ( V24() V32() ext-real ) Real) means :: RLAFFIN1:def 3
ex F being ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( ) set ) ) st
( F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) is one-to-one & rng F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = Carrier LS : ( ( ) ( ) set ) : ( ( ) ( ) Element of K19( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) & it : ( ( Function-like quasi_total ) ( Relation-like K20(S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) -defined S : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of K19(K20(K20(S : ( ( ) ( ) set ) ,S : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ,S : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) = Sum (LS : ( ( ) ( ) set ) * F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of S : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like FinSequence-like V55() V56() V57() ) FinSequence of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) );
end;

theorem :: RLAFFIN1:29
for S being ( ( non empty ) ( non empty ) addLoopStr )
for LS being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of S : ( ( non empty ) ( non empty ) addLoopStr ) )
for F being ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) st Carrier LS : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) : ( ( ) ( finite ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) misses rng F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) holds
Sum (LS : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) * F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like FinSequence-like V55() V56() V57() ) FinSequence of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) = 0 : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ;

theorem :: RLAFFIN1:30
for S being ( ( non empty ) ( non empty ) addLoopStr )
for LS being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of S : ( ( non empty ) ( non empty ) addLoopStr ) )
for F being ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) st F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) is one-to-one & Carrier LS : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) : ( ( ) ( finite ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= rng F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) holds
sum LS : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) : ( ( ) ( V24() V32() ext-real ) Real) = Sum (LS : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) * F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like FinSequence-like V55() V56() V57() ) FinSequence of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) ;

theorem :: RLAFFIN1:31
for S being ( ( non empty ) ( non empty ) addLoopStr ) holds sum (ZeroLC S : ( ( non empty ) ( non empty ) addLoopStr ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) : ( ( ) ( V24() V32() ext-real ) Real) = 0 : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ;

theorem :: RLAFFIN1:32
for S being ( ( non empty ) ( non empty ) addLoopStr )
for LS being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of S : ( ( non empty ) ( non empty ) addLoopStr ) )
for v being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st Carrier LS : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) : ( ( ) ( finite ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= {v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
sum LS : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) : ( ( ) ( V24() V32() ext-real ) Real) = LS : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) . v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) ;

theorem :: RLAFFIN1:33
for S being ( ( non empty ) ( non empty ) addLoopStr )
for LS being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of S : ( ( non empty ) ( non empty ) addLoopStr ) )
for v1, v2 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st Carrier LS : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) : ( ( ) ( finite ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= {v1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( finite ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & v1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> v2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
sum LS : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) : ( ( ) ( V24() V32() ext-real ) Real) = (LS : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) . v1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) + (LS : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) . v2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) ;

theorem :: RLAFFIN1:34
for S being ( ( non empty ) ( non empty ) addLoopStr )
for LS1, LS2 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of S : ( ( non empty ) ( non empty ) addLoopStr ) ) holds sum (LS1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) + LS2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) : ( ( ) ( V24() V32() ext-real ) Real) = (sum LS1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) ) : ( ( ) ( V24() V32() ext-real ) Real) + (sum LS2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty ) ( non empty ) addLoopStr ) ) ) : ( ( ) ( V24() V32() ext-real ) Real) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) ;

theorem :: RLAFFIN1:35
for r being ( ( ) ( V24() V32() ext-real ) Real)
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for L being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) holds sum (r : ( ( ) ( V24() V32() ext-real ) Real) * L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) : ( ( ) ( V24() V32() ext-real ) Real) = r : ( ( ) ( V24() V32() ext-real ) Real) * (sum L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( V24() V32() ext-real ) Real) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) ;

theorem :: RLAFFIN1:36
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for L1, L2 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) holds sum (L1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) - L2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) : ( ( ) ( V24() V32() ext-real ) Real) = (sum L1 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( V24() V32() ext-real ) Real) - (sum L2 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( V24() V32() ext-real ) Real) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) ;

theorem :: RLAFFIN1:37
for G being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr )
for LG being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of G : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) )
for g being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds sum LG : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) : ( ( ) ( V24() V32() ext-real ) Real) = sum (g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + LG : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() ) addLoopStr ) ) : ( ( ) ( V24() V32() ext-real ) Real) ;

theorem :: RLAFFIN1:38
for r being ( ( ) ( V24() V32() ext-real ) Real)
for R being ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct )
for LR being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of R : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) st r : ( ( ) ( V24() V32() ext-real ) Real) <> 0 : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
sum LR : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) : ( ( ) ( V24() V32() ext-real ) Real) = sum (r : ( ( ) ( V24() V32() ext-real ) Real) (*) LR : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) : ( ( ) ( V24() V32() ext-real ) Real) ;

theorem :: RLAFFIN1:39
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for L being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) holds Sum (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = ((sum L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( V24() V32() ext-real ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + (Sum L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:40
for r being ( ( ) ( V24() V32() ext-real ) Real)
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for L being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) holds Sum (r : ( ( ) ( V24() V32() ext-real ) Real) (*) L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = r : ( ( ) ( V24() V32() ext-real ) Real) * (Sum L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ;

begin

definition
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ;
let A be ( ( ) ( ) Subset of ) ;
attr A is affinely-independent means :: RLAFFIN1:def 4
( A : ( ( ) ( ) set ) is empty or ex v being ( ( ) ( ) VECTOR of ( ( ) ( ) set ) ) st
( v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) set ) & ((- v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) + A : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K19( the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) \ {(0. V : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of K19( the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) is linearly-independent ) );
end;

registration
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ;
cluster empty -> affinely-independent for ( ( ) ( ) Element of K19( the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
let v be ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ;
cluster {v : ( ( ) ( ) Element of the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) set ) -> affinely-independent for ( ( ) ( ) Subset of ) ;
let w be ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ;
cluster {v : ( ( ) ( ) Element of the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) Element of the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( finite ) set ) -> affinely-independent for ( ( ) ( ) Subset of ) ;
end;

registration
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ;
cluster 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element affinely-independent for ( ( ) ( ) Element of K19( the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: RLAFFIN1:41
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) is affinely-independent iff for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) holds
((- v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ {(0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) : ( ( ) ( V84(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element affinely-independent ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is linearly-independent ) ;

theorem :: RLAFFIN1:42
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) is affinely-independent iff for L being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of A : ( ( ) ( ) Subset of ) ) st Sum L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = 0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( V84(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) & sum L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( ) ( ) Subset of ) ) : ( ( ) ( V24() V32() ext-real ) Real) = 0 : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
Carrier L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( ) ( ) Subset of ) ) : ( ( ) ( finite ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( ) set ) ) ;

theorem :: RLAFFIN1:43
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is affinely-independent & B : ( ( ) ( ) Subset of ) c= A : ( ( ) ( ) Subset of ) holds
B : ( ( ) ( ) Subset of ) is affinely-independent ;

registration
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ;
cluster linearly-independent -> affinely-independent for ( ( ) ( ) Element of K19( the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ;
let I be ( ( affinely-independent ) ( affinely-independent ) Subset of ) ;
let v be ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ;
cluster v : ( ( ) ( ) Element of the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) + I : ( ( affinely-independent ) ( affinely-independent ) Element of K19( the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -> affinely-independent ;
end;

theorem :: RLAFFIN1:44
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) st v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is affinely-independent holds
A : ( ( ) ( ) Subset of ) is affinely-independent ;

registration
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ;
let I be ( ( affinely-independent ) ( affinely-independent ) Subset of ) ;
let r be ( ( ) ( V24() V32() ext-real ) Real) ;
cluster r : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) * I : ( ( affinely-independent ) ( affinely-independent ) Element of K19( the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -> affinely-independent ;
end;

theorem :: RLAFFIN1:45
for r being ( ( ) ( V24() V32() ext-real ) Real)
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) st r : ( ( ) ( V24() V32() ext-real ) Real) * A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is affinely-independent & r : ( ( ) ( V24() V32() ext-real ) Real) <> 0 : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
A : ( ( ) ( ) Subset of ) is affinely-independent ;

theorem :: RLAFFIN1:46
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) st 0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( V84(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) is affinely-independent iff A : ( ( ) ( ) Subset of ) \ {(0. V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) : ( ( ) ( V84(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element affinely-independent ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is linearly-independent ) ;

definition
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ;
let F be ( ( ) ( ) Subset-Family of ) ;
attr F is affinely-independent means :: RLAFFIN1:def 5
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) in F : ( ( ) ( ) set ) holds
A : ( ( ) ( ) Subset of ) is affinely-independent ;
end;

registration
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ;
cluster empty -> affinely-independent for ( ( ) ( ) Element of K19(K19( the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
let I be ( ( affinely-independent ) ( affinely-independent ) Subset of ) ;
cluster {I : ( ( affinely-independent ) ( affinely-independent ) Element of K19( the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) set ) -> affinely-independent for ( ( ) ( ) Subset-Family of ) ;
end;

registration
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ;
cluster empty affinely-independent for ( ( ) ( ) Element of K19(K19( the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
cluster non empty affinely-independent for ( ( ) ( ) Element of K19(K19( the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: RLAFFIN1:47
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for F1, F2 being ( ( ) ( ) Subset-Family of ) st F1 : ( ( ) ( ) Subset-Family of ) is affinely-independent & F2 : ( ( ) ( ) Subset-Family of ) is affinely-independent holds
F1 : ( ( ) ( ) Subset-Family of ) \/ F2 : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K19(K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is affinely-independent ;

theorem :: RLAFFIN1:48
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for F1, F2 being ( ( ) ( ) Subset-Family of ) st F1 : ( ( ) ( ) Subset-Family of ) c= F2 : ( ( ) ( ) Subset-Family of ) & F2 : ( ( ) ( ) Subset-Family of ) is affinely-independent holds
F1 : ( ( ) ( ) Subset-Family of ) is affinely-independent ;

begin

definition
let RLS be ( ( non empty ) ( non empty ) RLSStruct ) ;
let A be ( ( ) ( ) Subset of ) ;
func Affin A -> ( ( ) ( ) Subset of ) equals :: RLAFFIN1:def 6
meet { B : ( ( Affine ) ( Affine ) Subset of ) where B is ( ( Affine ) ( Affine ) Subset of ) : A : ( ( ) ( ) set ) c= B : ( ( Affine ) ( Affine ) Subset of ) } : ( ( ) ( ) set ) ;
end;

registration
let RLS be ( ( non empty ) ( non empty ) RLSStruct ) ;
let A be ( ( ) ( ) Subset of ) ;
cluster Affin A : ( ( ) ( ) Element of K19( the carrier of RLS : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) -> Affine ;
end;

registration
let RLS be ( ( non empty ) ( non empty ) RLSStruct ) ;
let A be ( ( empty ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty non trivial non finite V65() V66() V67() V68() V71() ) set ) -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} : ( ( ) ( ) set ) -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() ) Subset of ) ;
cluster Affin A : ( ( empty ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty non trivial non finite V65() V66() V67() V68() V71() ) set ) -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} : ( ( ) ( ) set ) -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() ) Element of K19( the carrier of RLS : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Affine ) Subset of ) -> empty ;
end;

registration
let RLS be ( ( non empty ) ( non empty ) RLSStruct ) ;
let A be ( ( non empty ) ( non empty ) Subset of ) ;
cluster Affin A : ( ( non empty ) ( non empty ) Element of K19( the carrier of RLS : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Affine ) Subset of ) -> non empty ;
end;

theorem :: RLAFFIN1:49
for RLS being ( ( non empty ) ( non empty ) RLSStruct )
for A being ( ( ) ( ) Subset of ) holds A : ( ( ) ( ) Subset of ) c= Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) ;

theorem :: RLAFFIN1:50
for RLS being ( ( non empty ) ( non empty ) RLSStruct )
for A being ( ( Affine ) ( Affine ) Subset of ) holds A : ( ( Affine ) ( Affine ) Subset of ) = Affin A : ( ( Affine ) ( Affine ) Subset of ) : ( ( ) ( Affine ) Subset of ) ;

theorem :: RLAFFIN1:51
for RLS being ( ( non empty ) ( non empty ) RLSStruct )
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) & B : ( ( ) ( ) Subset of ) is Affine holds
Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) c= B : ( ( ) ( ) Subset of ) ;

theorem :: RLAFFIN1:52
for RLS being ( ( non empty ) ( non empty ) RLSStruct )
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= B : ( ( ) ( ) Subset of ) holds
Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) c= Affin B : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) ;

theorem :: RLAFFIN1:53
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) holds Affin (v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Affine ) Subset of ) = v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (Affin A : ( ( ) ( ) Subset of ) ) : ( ( ) ( Affine ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:54
for r being ( ( ) ( V24() V32() ext-real ) Real)
for R being ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct )
for AR being ( ( ) ( ) Subset of ) st AR : ( ( ) ( ) Subset of ) is Affine holds
r : ( ( ) ( V24() V32() ext-real ) Real) * AR : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is Affine ;

theorem :: RLAFFIN1:55
for r being ( ( ) ( V24() V32() ext-real ) Real)
for R being ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct )
for AR being ( ( ) ( ) Subset of ) st r : ( ( ) ( V24() V32() ext-real ) Real) <> 0 : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
Affin (r : ( ( ) ( V24() V32() ext-real ) Real) * AR : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Affine ) Subset of ) = r : ( ( ) ( V24() V32() ext-real ) Real) * (Affin AR : ( ( ) ( ) Subset of ) ) : ( ( ) ( Affine ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:56
for r being ( ( ) ( V24() V32() ext-real ) Real)
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) holds Affin (r : ( ( ) ( V24() V32() ext-real ) Real) * A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Affine ) Subset of ) = r : ( ( ) ( V24() V32() ext-real ) Real) * (Affin A : ( ( ) ( ) Subset of ) ) : ( ( ) ( Affine ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:57
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) st v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) holds
Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) = v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + (Up (Lin ((- v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) Subspace of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( non empty ) ( non empty ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:58
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) is affinely-independent iff for B being ( ( ) ( ) Subset of ) st B : ( ( ) ( ) Subset of ) c= A : ( ( ) ( ) Subset of ) & Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) = Affin B : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) holds
A : ( ( ) ( ) Subset of ) = B : ( ( ) ( ) Subset of ) ) ;

theorem :: RLAFFIN1:59
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) holds Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) = { (Sum L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( ) ( ) Subset of ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) where L is ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of A : ( ( ) ( ) Subset of ) ) : sum L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( ) ( ) Subset of ) ) : ( ( ) ( V24() V32() ext-real ) Real) = 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) } ;

theorem :: RLAFFIN1:60
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of )
for I being ( ( affinely-independent ) ( affinely-independent ) Subset of ) st I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) c= A : ( ( ) ( ) Subset of ) holds
ex Ia being ( ( affinely-independent ) ( affinely-independent ) Subset of ) st
( I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) c= Ia : ( ( affinely-independent ) ( affinely-independent ) Subset of ) & Ia : ( ( affinely-independent ) ( affinely-independent ) Subset of ) c= A : ( ( ) ( ) Subset of ) & Affin Ia : ( ( affinely-independent ) ( affinely-independent ) Subset of ) : ( ( ) ( Affine ) Subset of ) = Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) ) ;

theorem :: RLAFFIN1:61
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A, B being ( ( finite ) ( finite ) Subset of ) st A : ( ( finite ) ( finite ) Subset of ) is affinely-independent & Affin A : ( ( finite ) ( finite ) Subset of ) : ( ( ) ( Affine ) Subset of ) = Affin B : ( ( finite ) ( finite ) Subset of ) : ( ( ) ( Affine ) Subset of ) & card B : ( ( finite ) ( finite ) Subset of ) : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of omega : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) set ) ) <= card A : ( ( finite ) ( finite ) Subset of ) : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of omega : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) set ) ) holds
B : ( ( finite ) ( finite ) Subset of ) is affinely-independent ;

theorem :: RLAFFIN1:62
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for L being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) holds
( L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) is convex iff ( sum L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) : ( ( ) ( V24() V32() ext-real ) Real) = 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) & ( for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds 0 : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) <= L : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) . v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) ) ) ) ;

theorem :: RLAFFIN1:63
for x being ( ( ) ( ) set )
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for L being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) st L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) is convex holds
L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) . x : ( ( ) ( ) set ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) <= 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ;

theorem :: RLAFFIN1:64
for x being ( ( ) ( ) set )
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for L being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) st L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) is convex & L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) . x : ( ( ) ( ) set ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) = 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
Carrier L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) : ( ( ) ( finite ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) set ) ;

theorem :: RLAFFIN1:65
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) holds conv A : ( ( ) ( ) Subset of ) : ( ( convex ) ( convex ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) ;

theorem :: RLAFFIN1:66
for x being ( ( ) ( ) set )
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) st x : ( ( ) ( ) set ) in conv A : ( ( ) ( ) Subset of ) : ( ( convex ) ( convex ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & (conv A : ( ( ) ( ) Subset of ) ) : ( ( convex ) ( convex ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) set ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is convex holds
x : ( ( ) ( ) set ) in A : ( ( ) ( ) Subset of ) ;

theorem :: RLAFFIN1:67
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A being ( ( ) ( ) Subset of ) holds Affin (conv A : ( ( ) ( ) Subset of ) ) : ( ( convex ) ( convex ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Affine ) Subset of ) = Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) ;

theorem :: RLAFFIN1:68
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A, B being ( ( ) ( ) Subset of ) st conv A : ( ( ) ( ) Subset of ) : ( ( convex ) ( convex ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= conv B : ( ( ) ( ) Subset of ) : ( ( convex ) ( convex ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) c= Affin B : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) ;

theorem :: RLAFFIN1:69
for RLS being ( ( non empty ) ( non empty ) RLSStruct )
for A, B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= Affin B : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) holds
Affin (A : ( ( ) ( ) Subset of ) \/ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Affine ) Subset of ) = Affin B : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) ;

begin

definition
let V be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ;
let A be ( ( ) ( ) Subset of ) ;
assume A : ( ( ) ( ) Subset of ) is affinely-independent ;
let x be ( ( ) ( ) set ) ;
assume x : ( ( ) ( ) set ) in Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) ;
func x |-- A -> ( ( ) ( Relation-like the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of A : ( ( ) ( ) set ) ) means :: RLAFFIN1:def 7
( Sum it : ( ( Function-like quasi_total ) ( Relation-like K20(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) ) : ( ( ) ( Relation-like ) set ) -defined V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) -valued Function-like quasi_total ) Element of K19(K20(K20(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) ) : ( ( ) ( Relation-like ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) & sum it : ( ( Function-like quasi_total ) ( Relation-like K20(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) ) : ( ( ) ( Relation-like ) set ) -defined V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) -valued Function-like quasi_total ) Element of K19(K20(K20(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) ) : ( ( ) ( Relation-like ) set ) ,V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RLSStruct ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V32() ext-real ) Real) = 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) );
end;

theorem :: RLAFFIN1:70
for r being ( ( ) ( V24() V32() ext-real ) Real)
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for v1, v2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for I being ( ( affinely-independent ) ( affinely-independent ) Subset of ) st v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Affin I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) : ( ( ) ( Affine ) Subset of ) & v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Affin I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) : ( ( ) ( Affine ) Subset of ) holds
(((1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) - r : ( ( ) ( V24() V32() ext-real ) Real) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) * v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + (r : ( ( ) ( V24() V32() ext-real ) Real) * v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) |-- I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b5 : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) = ((1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) - r : ( ( ) ( V24() V32() ext-real ) Real) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) * (v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) |-- I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b5 : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) + (r : ( ( ) ( V24() V32() ext-real ) Real) * (v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) |-- I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b5 : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ;

theorem :: RLAFFIN1:71
for x being ( ( ) ( ) set )
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for I being ( ( affinely-independent ) ( affinely-independent ) Subset of ) st x : ( ( ) ( ) set ) in conv I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) : ( ( convex ) ( convex ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) set ) |-- I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b4 : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) is convex & 0 : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) <= (x : ( ( ) ( ) set ) |-- I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b4 : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) . v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) & (x : ( ( ) ( ) set ) |-- I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b4 : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) . v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) <= 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) ;

theorem :: RLAFFIN1:72
for x, y being ( ( ) ( ) set )
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for I being ( ( affinely-independent ) ( affinely-independent ) Subset of ) st x : ( ( ) ( ) set ) in conv I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) : ( ( convex ) ( convex ) Element of K19( the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
( (x : ( ( ) ( ) set ) |-- I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b4 : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) . y : ( ( ) ( ) set ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) = 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) iff ( x : ( ( ) ( ) set ) = y : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) in I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) ) ;

theorem :: RLAFFIN1:73
for x being ( ( ) ( ) set )
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for I being ( ( affinely-independent ) ( affinely-independent ) Subset of ) st x : ( ( ) ( ) set ) in Affin I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) : ( ( ) ( Affine ) Subset of ) & ( for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) st v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) holds
0 : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) <= (x : ( ( ) ( ) set ) |-- I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) . v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) ) holds
x : ( ( ) ( ) set ) in conv I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) : ( ( convex ) ( convex ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:74
for x being ( ( ) ( ) set )
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for I being ( ( affinely-independent ) ( affinely-independent ) Subset of ) st x : ( ( ) ( ) set ) in I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) holds
(conv I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) : ( ( convex ) ( convex ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) set ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is convex ;

theorem :: RLAFFIN1:75
for x being ( ( ) ( ) set )
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for I being ( ( affinely-independent ) ( affinely-independent ) Subset of )
for B being ( ( ) ( ) Subset of ) st x : ( ( ) ( ) set ) in Affin I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) : ( ( ) ( Affine ) Subset of ) & ( for y being ( ( ) ( ) set ) st y : ( ( ) ( ) set ) in B : ( ( ) ( ) Subset of ) holds
(x : ( ( ) ( ) set ) |-- I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) . y : ( ( ) ( ) set ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) = 0 : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) holds
( x : ( ( ) ( ) set ) in Affin (I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) \ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Affine ) Subset of ) & x : ( ( ) ( ) set ) |-- I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) = x : ( ( ) ( ) set ) |-- (I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) \ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( affinely-independent ) ( affinely-independent ) Subset of ) \ b4 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: RLAFFIN1:76
for x being ( ( ) ( ) set )
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for I being ( ( affinely-independent ) ( affinely-independent ) Subset of )
for B being ( ( ) ( ) Subset of ) st x : ( ( ) ( ) set ) in conv I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) : ( ( convex ) ( convex ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & ( for y being ( ( ) ( ) set ) st y : ( ( ) ( ) set ) in B : ( ( ) ( ) Subset of ) holds
(x : ( ( ) ( ) set ) |-- I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) . y : ( ( ) ( ) set ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) = 0 : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) holds
x : ( ( ) ( ) set ) in conv (I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) \ B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( convex ) ( convex ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLAFFIN1:77
for x being ( ( ) ( ) set )
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for B being ( ( ) ( ) Subset of )
for I being ( ( affinely-independent ) ( affinely-independent ) Subset of ) st B : ( ( ) ( ) Subset of ) c= I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) & x : ( ( ) ( ) set ) in Affin B : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) holds
x : ( ( ) ( ) set ) |-- B : ( ( ) ( ) Subset of ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( ) ( ) Subset of ) ) = x : ( ( ) ( ) set ) |-- I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b4 : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) ;

theorem :: RLAFFIN1:78
for r, s being ( ( ) ( V24() V32() ext-real ) Real)
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for v1, v2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) st v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) & v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) & r : ( ( ) ( V24() V32() ext-real ) Real) + s : ( ( ) ( V24() V32() ext-real ) Real) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) = 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) holds
(r : ( ( ) ( V24() V32() ext-real ) Real) * v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + (s : ( ( ) ( V24() V32() ext-real ) Real) * v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) in Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) ;

theorem :: RLAFFIN1:79
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A, B being ( ( finite ) ( finite ) Subset of ) st A : ( ( finite ) ( finite ) Subset of ) is affinely-independent & Affin A : ( ( finite ) ( finite ) Subset of ) : ( ( ) ( Affine ) Subset of ) c= Affin B : ( ( finite ) ( finite ) Subset of ) : ( ( ) ( Affine ) Subset of ) holds
card A : ( ( finite ) ( finite ) Subset of ) : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of omega : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) set ) ) <= card B : ( ( finite ) ( finite ) Subset of ) : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of omega : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) set ) ) ;

theorem :: RLAFFIN1:80
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for A, B being ( ( finite ) ( finite ) Subset of ) st A : ( ( finite ) ( finite ) Subset of ) is affinely-independent & Affin A : ( ( finite ) ( finite ) Subset of ) : ( ( ) ( Affine ) Subset of ) c= Affin B : ( ( finite ) ( finite ) Subset of ) : ( ( ) ( Affine ) Subset of ) & card A : ( ( finite ) ( finite ) Subset of ) : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of omega : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) set ) ) = card B : ( ( finite ) ( finite ) Subset of ) : ( ( ) ( V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of omega : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) set ) ) holds
B : ( ( finite ) ( finite ) Subset of ) is affinely-independent ;

theorem :: RLAFFIN1:81
for r, s being ( ( ) ( V24() V32() ext-real ) Real)
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for L1, L2 being ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of V : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) st L1 : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) . v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) <> L2 : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) . v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) holds
( ((r : ( ( ) ( V24() V32() ext-real ) Real) * L1 : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) + ((1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) - r : ( ( ) ( V24() V32() ext-real ) Real) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) * L2 : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) ) : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) . v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) = s : ( ( ) ( V24() V32() ext-real ) Real) iff r : ( ( ) ( V24() V32() ext-real ) Real) = ((L2 : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) . v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) - s : ( ( ) ( V24() V32() ext-real ) Real) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) / ((L2 : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) . v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) - (L1 : ( ( ) ( Relation-like the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ) . v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) ) ;

theorem :: RLAFFIN1:82
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) holds
( A : ( ( ) ( ) Subset of ) \/ {v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element affinely-independent ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is affinely-independent iff ( A : ( ( ) ( ) Subset of ) is affinely-independent & ( v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) or not v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) ) ) ) ;

theorem :: RLAFFIN1:83
for r, s being ( ( ) ( V24() V32() ext-real ) Real)
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for w, v1, v2 being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) st not w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Affin A : ( ( ) ( ) Subset of ) : ( ( ) ( Affine ) Subset of ) & v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) & v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) & r : ( ( ) ( V24() V32() ext-real ) Real) <> 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) & (r : ( ( ) ( V24() V32() ext-real ) Real) * w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + ((1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) - r : ( ( ) ( V24() V32() ext-real ) Real) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) * v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) = (s : ( ( ) ( V24() V32() ext-real ) Real) * w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + ((1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) - s : ( ( ) ( V24() V32() ext-real ) Real) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) * v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) holds
( r : ( ( ) ( V24() V32() ext-real ) Real) = s : ( ( ) ( V24() V32() ext-real ) Real) & v1 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = v2 : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) ;

theorem :: RLAFFIN1:84
for r being ( ( ) ( V24() V32() ext-real ) Real)
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace)
for v, w, p being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) )
for I being ( ( affinely-independent ) ( affinely-independent ) Subset of ) st v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) & w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Affin I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) : ( ( ) ( Affine ) Subset of ) & p : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) in Affin (I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) \ {v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element affinely-independent ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Affine ) Subset of ) & w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = (r : ( ( ) ( V24() V32() ext-real ) Real) * v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) + ((1 : ( ( ) ( non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() ) Element of K19(REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) - r : ( ( ) ( V24() V32() ext-real ) Real) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) * p : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) ) holds
r : ( ( ) ( V24() V32() ext-real ) Real) = (w : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) |-- I : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) -valued Function-like total quasi_total V55() V56() V57() ) Linear_Combination of b6 : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) . v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( V24() V32() ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V65() V66() V67() V71() ) set ) ) ;