let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; for a being Element of L
for p, q being FinSequence of L st len p = len q & ( for i being Element of NAT st i in dom p holds
q /. i = a * (p /. i) ) holds
Sum q = a * (Sum p)
let a be Element of L; for p, q being FinSequence of L st len p = len q & ( for i being Element of NAT st i in dom p holds
q /. i = a * (p /. i) ) holds
Sum q = a * (Sum p)
let p, q be FinSequence of L; ( len p = len q & ( for i being Element of NAT st i in dom p holds
q /. i = a * (p /. i) ) implies Sum q = a * (Sum p) )
assume A1:
( len p = len q & ( for i being Element of NAT st i in dom p holds
q /. i = a * (p /. i) ) )
; Sum q = a * (Sum p)
consider fq being sequence of the carrier of L such that
A2:
Sum q = fq . (len q)
and
A3:
fq . 0 = 0. L
and
A4:
for j being Nat
for v being Element of L st j < len q & v = q . (j + 1) holds
fq . (j + 1) = (fq . j) + v
by RLVECT_1:def 12;
consider fp being sequence of the carrier of L such that
A5:
Sum p = fp . (len p)
and
A6:
fp . 0 = 0. L
and
A7:
for j being Nat
for v being Element of L st j < len p & v = p . (j + 1) holds
fp . (j + 1) = (fp . j) + v
by RLVECT_1:def 12;
defpred S1[ Element of NAT ] means fq . $1 = a * (fp . $1);
A8:
S1[ 0 ]
by A6, A3;
A9:
for j being Element of NAT st 0 <= j & j < len p & S1[j] holds
S1[j + 1]
proof
let j be
Element of
NAT ;
( 0 <= j & j < len p & S1[j] implies S1[j + 1] )
assume A10:
(
0 <= j &
j < len p )
;
( not S1[j] or S1[j + 1] )
assume A11:
S1[
j]
;
S1[j + 1]
A12:
1
<= j + 1
by NAT_1:11;
A13:
j + 1
<= len p
by A10, NAT_1:13;
then
j + 1
in Seg (len q)
by A12, A1;
then A14:
j + 1
in dom q
by FINSEQ_1:def 3;
j + 1
in Seg (len p)
by A12, A13;
then A15:
j + 1
in dom p
by FINSEQ_1:def 3;
set vq =
q /. (j + 1);
set vp =
p /. (j + 1);
A16:
q /. (j + 1) = q . (j + 1)
by A14, PARTFUN1:def 6;
A17:
p /. (j + 1) = p . (j + 1)
by A15, PARTFUN1:def 6;
fq . (j + 1) =
(a * (fp . j)) + (q /. (j + 1))
by A11, A1, A16, A10, A4
.=
(a * (fp . j)) + (a * (p /. (j + 1)))
by A1, A15
.=
a * ((fp . j) + (p /. (j + 1)))
by VECTSP_1:def 2
.=
a * (fp . (j + 1))
by A17, A10, A7
;
hence
S1[
j + 1]
;
verum
end;
for j being Element of NAT st 0 <= j & j <= len p holds
S1[j]
from INT_1:sch 7(A8, A9);
hence
Sum q = a * (Sum p)
by A1, A5, A2; verum