let R be non empty commutative doubleLoopStr ; :: thesis: for a being Element of R
for p being FinSequence of the carrier of R holds Sum (p * a) = Sum (a * p)
let a be Element of R; :: thesis: for p being FinSequence of the carrier of R holds Sum (p * a) = Sum (a * p)
let p be FinSequence of the carrier of R; :: thesis: Sum (p * a) = Sum (a * p)
consider f being Function of NAT, the carrier of R such that
A1: Sum (p * a) = f . (len (p * a)) and
A2: f . 0 = 0. R and
A3: for j being Element of NAT
for v being Element of R st j < len (p * a) & v = (p * a) . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def 15;
consider g being Function of NAT, the carrier of R such that
A4: Sum (a * p) = g . (len (a * p)) and
A5: g . 0 = 0. R and
A6: for j being Element of NAT
for v being Element of R st j < len (a * p) & v = (a * p) . (j + 1) holds
g . (j + 1) = (g . j) + v by RLVECT_1:def 15;
defpred S₁[ Element of NAT ] means f . $1 = g . $1;
A7: Seg (len (p * a)) = dom (p * a) by FINSEQ_1:def 3
.= dom p by POLYNOM1:def 3
.= Seg (len p) by FINSEQ_1:def 3 ;
A8: Seg (len (a * p)) = dom (a * p) by FINSEQ_1:def 3
.= dom p by POLYNOM1:def 2
.= Seg (len p) by FINSEQ_1:def 3 ;

A9: now

let j be Element of NAT ; :: thesis: ( 0 <= j & j < len p & S₁[j] implies S₁[j + 1] )
assume that
0 <= j and
A10: j < len p ; :: thesis: ( S₁[j] implies S₁[j + 1] )
thus ( S₁[j] implies S₁[j + 1] ) :: thesis: verum

proof

A11: j < len (a * p) by A8, A10, FINSEQ_1:8;
A12: j < len (p * a) by A7, A10, FINSEQ_1:8;
then A13: j + 1 <= len (p * a) by NAT_1:13;
A14: 0 + 1 <= j + 1 by XREAL_1:8;
then j + 1 in Seg (len (p * a)) by A13, FINSEQ_1:3;
then j + 1 in dom (p * a) by FINSEQ_1:def 3;
then A15: (p * a) /. (j + 1) = (p * a) . (j + 1) by PARTFUN1:def 8;
j + 1 in Seg (len (a * p)) by A8, A7, A13, A14, FINSEQ_1:3;
then A16: j + 1 in dom (a * p) by FINSEQ_1:def 3;
then A17: j + 1 in dom p by POLYNOM1:def 2;
A18: (a * p) /. (j + 1) = (a * p) . (j + 1) by A16, PARTFUN1:def 8;
assume f . j = g . j ; :: thesis: S₁[j + 1]
hence f . (j + 1) = (g . j) + ((p * a) /. (j + 1)) by A3, A12, A15
.= (g . j) + ((p /. (j + 1)) * a) by A17, POLYNOM1:def 3
.= (g . j) + ((a * p) /. (j + 1)) by A17, POLYNOM1:def 2
.= g . (j + 1) by A6, A11, A18 ;
:: thesis: verum

end;

end;

A19: S₁[ 0 ] by A2, A5;
A20: for i being Element of NAT st 0 <= i & i <= len p holds
S₁[i] from INT_1:sch 7(A19, A9);
thus Sum (p * a) = f . (len p) by A1, A7, FINSEQ_1:8
.= g . (len p) by A20
.= Sum (a * p) by A4, A8, FINSEQ_1:8 ; :: thesis: verum