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)) & f . 0 = 0. R & ( 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 13;
consider g being Function of NAT ,the carrier of R such that
A2:
( Sum (a * p) = g . (len (a * p)) & g . 0 = 0. R & ( 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 13;
A3: 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
;
A4: 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
;
defpred S1[ Element of NAT ] means f . $1 = g . $1;
A5:
S1[ 0 ]
by A1, A2;
A6:
now let j be
Element of
NAT ;
:: thesis: ( 0 <= j & j < len p & S1[j] implies S1[j + 1] )assume A7:
(
0 <= j &
j < len p )
;
:: thesis: ( S1[j] implies S1[j + 1] )thus
(
S1[
j] implies
S1[
j + 1] )
:: thesis: verumproof
assume A8:
f . j = g . j
;
:: thesis: S1[j + 1]
A9:
j < len (p * a)
by A4, A7, FINSEQ_1:8;
then A10:
j + 1
<= len (p * a)
by NAT_1:13;
A11:
0 + 1
<= j + 1
by XREAL_1:8;
then
j + 1
in Seg (len (p * a))
by A10, FINSEQ_1:3;
then
j + 1
in dom (p * a)
by FINSEQ_1:def 3;
then A12:
(p * a) /. (j + 1) = (p * a) . (j + 1)
by PARTFUN1:def 8;
A13:
j < len (a * p)
by A3, A7, FINSEQ_1:8;
j + 1
in Seg (len (a * p))
by A3, A4, A10, A11, FINSEQ_1:3;
then A14:
j + 1
in dom (a * p)
by FINSEQ_1:def 3;
then A15:
j + 1
in dom p
by POLYNOM1:def 2;
A16:
(a * p) /. (j + 1) = (a * p) . (j + 1)
by A14, PARTFUN1:def 8;
thus f . (j + 1) =
(g . j) + ((p * a) /. (j + 1))
by A1, A8, A9, A12
.=
(g . j) + ((p /. (j + 1)) * a)
by A15, POLYNOM1:def 3
.=
(g . j) + ((a * p) /. (j + 1))
by A15, POLYNOM1:def 2
.=
g . (j + 1)
by A2, A13, A16
;
:: thesis: verum
end; end;
A17:
for i being Element of NAT st 0 <= i & i <= len p holds
S1[i]
from POLYNOM2:sch 4(A5, A6);
thus Sum (p * a) =
f . (len p)
by A1, A4, FINSEQ_1:8
.=
g . (len p)
by A17
.=
Sum (a * p)
by A2, A3, FINSEQ_1:8
; :: thesis: verum