let K be Ring; :: thesis: for a being Element of K
for p1, p2 being FinSequence of the carrier of K st len p1 = len p2 & ( for i being Element of NAT
for k being Element of K st i in dom p1 & k = p1 . i holds
p2 . i = k * a ) holds
Sum p2 = (Sum p1) * a
let a be Element of K; :: thesis: for p1, p2 being FinSequence of the carrier of K st len p1 = len p2 & ( for i being Element of NAT
for k being Element of K st i in dom p1 & k = p1 . i holds
p2 . i = k * a ) holds
Sum p2 = (Sum p1) * a
defpred S₁[ FinSequence of the carrier of K] means for p2 being FinSequence of the carrier of K st len $1 = len p2 & ( for i being Element of NAT
for k being Element of K st i in dom $1 & k = $1 . i holds
p2 . i = k * a ) holds
Sum p2 = (Sum $1) * a;
A1: S₁[ <*> the carrier of K]

proof

A2: Sum (<*> the carrier of K) = 0. K by RLVECT_1:43;

now :: thesis: for p2 being FinSequence of the carrier of K st len (<*> the carrier of K) = len p2 holds
Sum p2 = (Sum (<*> the carrier of K)) * a

let p2 be FinSequence of the carrier of K; :: thesis: ( len (<*> the carrier of K) = len p2 implies Sum p2 = (Sum (<*> the carrier of K)) * a )
assume len (<*> the carrier of K) = len p2 ; :: thesis: Sum p2 = (Sum (<*> the carrier of K)) * a
then p2 = <*> the carrier of K ;
hence Sum p2 = (Sum (<*> the carrier of K)) * a by A2; :: thesis: verum

end;

hence S₁[ <*> the carrier of K] ; :: thesis: verum

end;

A3: for p being FinSequence of the carrier of K
for x being Element of the carrier of K st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of the carrier of K; :: thesis: for x being Element of the carrier of K st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of the carrier of K; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A4: S₁[p] ; :: thesis: S₁[p ^ <*x*>]
for p2 being FinSequence of the carrier of K st len (p ^ <*x*>) = len p2 & ( for i being Element of NAT
for k being Element of K st i in dom (p ^ <*x*>) & k = (p ^ <*x*>) . i holds
p2 . i = k * a ) holds
Sum p2 = (Sum (p ^ <*x*>)) * a

proof

let p2 be FinSequence of the carrier of K; :: thesis: ( len (p ^ <*x*>) = len p2 & ( for i being Element of NAT
for k being Element of K st i in dom (p ^ <*x*>) & k = (p ^ <*x*>) . i holds
p2 . i = k * a ) implies Sum p2 = (Sum (p ^ <*x*>)) * a )
assume that
A5: len (p ^ <*x*>) = len p2 and
A6: for i being Element of NAT
for k being Element of K st i in dom (p ^ <*x*>) & k = (p ^ <*x*>) . i holds
p2 . i = k * a ; :: thesis: Sum p2 = (Sum (p ^ <*x*>)) * a
len p2 <> 0 by A5;
then consider q being FinSequence of the carrier of K, d being Element of K such that
A7: p2 = q ^ <*d*> by FINSEQ_2:19;
(len q) + 1 = len p2 by A7, FINSEQ_2:16
.= (len p) + 1 by A5, FINSEQ_2:16 ;
then A8: len p = len q by XCMPLX_1:2;
for i being Element of NAT
for k being Element of K st i in dom p & k = p . i holds
q . i = k * a

proof

let i be Element of NAT ; :: thesis: for k being Element of K st i in dom p & k = p . i holds
q . i = k * a
let k be Element of K; :: thesis: ( i in dom p & k = p . i implies q . i = k * a )
assume that
A9: i in dom p and
A10: k = p . i ; :: thesis: q . i = k * a
A11: i in dom (p ^ <*x*>) by A9, FINSEQ_2:15;
i in Seg (len p) by A9, FINSEQ_1:def 3;
then A12: ( 1 <= i & i <= len p ) by FINSEQ_1:1;
then A13: (p ^ <*x*>) . i = k by A10, FINSEQ_1:64;
thus q . i = (q ^ <*d*>) . i by A12, A8, FINSEQ_1:64
.= k * a by A7, A13, A6, A11 ; :: thesis: verum

end;

then A14: Sum q = (Sum p) * a by A4, A8;
set p1 = p ^ <*x*>;
reconsider i1 = (len p) + 1 as Element of NAT ;
len <*x*> = 1 by FINSEQ_1:40;
then dom <*x*> = Seg 1 by FINSEQ_1:def 3;
then 1 in dom <*x*> by FINSEQ_1:3;
then ( (len p) + 1 in dom (p ^ <*x*>) & x = (p ^ <*x*>) . ((len p) + 1) ) by FINSEQ_1:28, FINSEQ_1:42;
then ( i1 in dom (p ^ <*x*>) & x = (p ^ <*x*>) . i1 ) ;
then A15: p2 . i1 = x * a by A6;
d = p2 . i1 by A7, A8, FINSEQ_1:42;
then A16: d = x * a by A15;
thus Sum p2 = (Sum q) + d by A7, FVSUM_1:71
.= ((Sum p) + x) * a by A14, A16, VECTSP_1:def 3
.= (Sum (p ^ <*x*>)) * a by FVSUM_1:71 ; :: thesis: verum

end;

hence S₁[p ^ <*x*>] ; :: thesis: verum

end;

thus for p being FinSequence of the carrier of K holds S₁[p] from FINSEQ_2:sch 2(A1, A3); :: thesis: verum