let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ) ) ; :: thesis: 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 S₁[ Element of NAT ] means fq . $1 = a * (fp . $1);
A8: S₁[ 0 ] by A6, A3;
A9: for j being Element of NAT st 0 <= j & j < len p & S₁[j] holds
S₁[j + 1]

proof

let j be Element of NAT ; :: thesis: ( 0 <= j & j < len p & S₁[j] implies S₁[j + 1] )
assume A10: ( 0 <= j & j < len p ) ; :: thesis: ( not S₁[j] or S₁[j + 1] )
assume A11: S₁[j] ; :: thesis: S₁[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 S₁[j + 1] ; :: thesis: verum

end;

for j being Element of NAT st 0 <= j & j <= len p holds
S₁[j] from INT_1:sch 7(A8, A9);
hence Sum q = a * (Sum p) by A1, A5, A2; :: thesis: verum