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

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