let S be non empty addLoopStr ; 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; 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; ( 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
; 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; verum