let d be XFinSequence of REAL ; :: thesis: for k being Nat st len d = k + 1 holds
ex a being Real ex d1 being XFinSequence of REAL ex y being Real_Sequence st
( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> & seq_p d = (seq_p d1) + y & ( for i being Nat holds y . i = a * (i to_power k) ) )
let k be Nat; :: thesis: ( len d = k + 1 implies ex a being Real ex d1 being XFinSequence of REAL ex y being Real_Sequence st
( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> & seq_p d = (seq_p d1) + y & ( for i being Nat holds y . i = a * (i to_power k) ) ) )
assume AS: len d = k + 1 ; :: thesis: ex a being Real ex d1 being XFinSequence of REAL ex y being Real_Sequence st
( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> & seq_p d = (seq_p d1) + y & ( for i being Nat holds y . i = a * (i to_power k) ) )
then consider a being Real, d1 being XFinSequence of REAL such that
P1: ( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> ) by LMXFIN3;
deffunc H₁( Nat) -> set = a * ($1 to_power k);
consider y being Real_Sequence such that
P3: for x being Nat holds y . x = H₁(x) from SEQ_1:sch 1();
for x being Element of NAT holds (seq_p d) . x = ((seq_p d1) + y) . x

proof

let x be Element of NAT ; :: thesis: (seq_p d) . x = ((seq_p d1) + y) . x
Q1: (seq_p d) . x = Sum (d (#) (seq_a^ (x,1,0))) by defseqp;
Q2: (seq_p d1) . x = Sum (d1 (#) (seq_a^ (x,1,0))) by defseqp;
Q3: len (d (#) (seq_a^ (x,1,0))) = k + 1 by AS, LMXFIN1;
K1: k < k + 1 by NAT_1:13;
then k in Segm (k + 1) by NAT_1:44;
then Q6: (d (#) (seq_a^ (x,1,0))) . k = a * (x to_power k) by AS, P1, LMXFIN2;
Q5: d (#) (seq_a^ (x,1,0)) = ((d (#) (seq_a^ (x,1,0))) | k) ^ <%(a * (x to_power k))%> by Q6, Q3, AFINSQ_1:56;
Q7: len ((d (#) (seq_a^ (x,1,0))) | k) = k by AFINSQ_1:54, Q3, K1;
for i being object st i in dom ((d (#) (seq_a^ (x,1,0))) | k) holds
((d (#) (seq_a^ (x,1,0))) | k) . i = (d1 (#) (seq_a^ (x,1,0))) . i

proof

let i be object ; :: thesis: ( i in dom ((d (#) (seq_a^ (x,1,0))) | k) implies ((d (#) (seq_a^ (x,1,0))) | k) . i = (d1 (#) (seq_a^ (x,1,0))) . i )
assume A1: i in dom ((d (#) (seq_a^ (x,1,0))) | k) ; :: thesis: ((d (#) (seq_a^ (x,1,0))) | k) . i = (d1 (#) (seq_a^ (x,1,0))) . i
then i in dom (d (#) (seq_a^ (x,1,0))) by RELAT_1:57;
then A2: i in dom d by LMXFIN1;
reconsider i0 = i as Nat by A1;
thus ((d (#) (seq_a^ (x,1,0))) | k) . i = (d (#) (seq_a^ (x,1,0))) . i by A1, FUNCT_1:47
.= (d . i) * (x to_power i0) by A2, LMXFIN2
.= (d1 . i) * (x to_power i0) by FUNCT_1:47, A1, P1, Q7
.= (d1 (#) (seq_a^ (x,1,0))) . i by LMXFIN2, A1, P1, Q7 ; :: thesis: verum

end;

then (d (#) (seq_a^ (x,1,0))) | k = d1 (#) (seq_a^ (x,1,0)) by P1, LMXFIN1, Q7;
hence (seq_p d) . x = (Sum (d1 (#) (seq_a^ (x,1,0)))) + (Sum <%(a * (x to_power k))%>) by Q1, Q5, AFINSQ_2:55
.= ((seq_p d1) . x) + (a * (x to_power k)) by AFINSQ_2:53, Q2
.= ((seq_p d1) . x) + (y . x) by P3
.= ((seq_p d1) + y) . x by SEQ_1:7 ;
:: thesis: verum

end;

then seq_p d = (seq_p d1) + y ;
hence ex a being Real ex d1 being XFinSequence of REAL ex y being Real_Sequence st
( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> & seq_p d = (seq_p d1) + y & ( for i being Nat holds y . i = a * (i to_power k) ) ) by P1, P3; :: thesis: verum