let S be non empty addLoopStr ; :: thesis: for LS being Linear_Combination of S
for v1, v2 being Element of S st Carrier LS c= {v1,v2} & v1 <> v2 holds
sum LS = (LS . v1) + (LS . v2)
let LS be Linear_Combination of S; :: thesis: for v1, v2 being Element of S st Carrier LS c= {v1,v2} & v1 <> v2 holds
sum LS = (LS . v1) + (LS . v2)
let v1, v2 be Element of S; :: thesis: ( Carrier LS c= {v1,v2} & v1 <> v2 implies sum LS = (LS . v1) + (LS . v2) )
consider p being FinSequence such that
A1: rng p = {v1,v2} and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of S by A1, FINSEQ_1:def 4;
assume that
A3: Carrier LS c= {v1,v2} and
A4: v1 <> v2 ; :: thesis: sum LS = (LS . v1) + (LS . v2)
A5: dom LS = the carrier of S by FUNCT_2:def 1;
A6: Sum <*(LS . v1)*> = LS . v1 by RVSUM_1:73;
( p = <*v1,v2*> or p = <*v2,v1*> ) by A1, A2, A4, FINSEQ_3:99;
then ( LS * p = <*(LS . v1),(LS . v2)*> or LS * p = <*(LS . v2),(LS . v1)*> ) by A5, FINSEQ_2:125;
then ( Sum (LS * p) = (LS . v1) + (LS . v2) or Sum (LS * p) = (LS . v2) + (LS . v1) ) by A6, RVSUM_1:74, RVSUM_1:76;
hence sum LS = (LS . v1) + (LS . v2) by A1, A2, A3, Th30; :: thesis: verum