defpred S1[ Nat] means for c, absc being XFinSequence of REAL st len c = $1 & absc = |.c.| holds
for x being Nat holds |.((seq_p c) . x).| <= (seq_p absc) . x;
P0: S1[ 0 ]
proof
let c, absc be XFinSequence of REAL ; :: thesis: ( len c = 0 & absc = |.c.| implies for x being Nat holds |.((seq_p c) . x).| <= (seq_p absc) . x )
assume A0: ( len c = 0 & absc = |.c.| ) ; :: thesis: for x being Nat holds |.((seq_p c) . x).| <= (seq_p absc) . x
D2: dom absc = {} by A0, VALUED_1:def 11;
let x be Nat; :: thesis: |.((seq_p c) . x).| <= (seq_p absc) . x
c (#) (seq_a^ (x,1,0)) = {} by A0, LMXFIN1;
then Q2: Sum (c (#) (seq_a^ (x,1,0))) = 0 ;
absc (#) (seq_a^ (x,1,0)) = {} by D2, LMXFIN1;
then Q3: Sum (absc (#) (seq_a^ (x,1,0))) = 0 ;
|.((seq_p c) . x).| = 0 by COMPLEX1:44, Q2, defseqp;
hence |.((seq_p c) . x).| <= (seq_p absc) . x by Q3, defseqp; :: thesis: verum
end;
P1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A0: S1[k] ; :: thesis: S1[k + 1]
let c, absc be XFinSequence of REAL ; :: thesis: ( len c = k + 1 & absc = |.c.| implies for x being Nat holds |.((seq_p c) . x).| <= (seq_p absc) . x )
assume A1: ( len c = k + 1 & absc = |.c.| ) ; :: thesis: for x being Nat holds |.((seq_p c) . x).| <= (seq_p absc) . x
consider a1 being Real, c1 being XFinSequence of REAL , y1 being Real_Sequence such that
A2: ( len c1 = k & c1 = c | k & a1 = c . k & c = c1 ^ <%a1%> & seq_p c = (seq_p c1) + y1 & ( for i being Nat holds y1 . i = a1 * (i to_power k) ) ) by A1, LMXFIN4;
len absc = k + 1 by A1, VALUED_1:def 11;
then consider a2 being Real, c2 being XFinSequence of REAL , y2 being Real_Sequence such that
A4: ( len c2 = k & c2 = absc | k & a2 = absc . k & absc = c2 ^ <%a2%> & seq_p absc = (seq_p c2) + y2 & ( for i being Nat holds y2 . i = a2 * (i to_power k) ) ) by LMXFIN4;
A5: |.a1.| = a2 by A1, A2, A4, VALUED_1:18;
for i being object st i in dom c2 holds
c2 . i = |.(c1 . i).|
proof
let i be object ; :: thesis: ( i in dom c2 implies c2 . i = |.(c1 . i).| )
assume B1: i in dom c2 ; :: thesis: c2 . i = |.(c1 . i).|
c2 . i = absc . i by A4, B1, FUNCT_1:47
.= |.(c . i).| by A1, VALUED_1:18
.= |.(c1 . i).| by A2, B1, FUNCT_1:47, A4 ;
hence c2 . i = |.(c1 . i).| ; :: thesis: verum
end;
then AA7: c2 = |.c1.| by VALUED_1:def 11, A2, A4;
let x be Nat; :: thesis: |.((seq_p c) . x).| <= (seq_p absc) . x
A8: (seq_p c) . x = ((seq_p c1) . x) + (y1 . x) by SEQ_1:7, A2;
A9: (seq_p absc) . x = ((seq_p c2) . x) + (y2 . x) by SEQ_1:7, A4;
A10: |.((seq_p c) . x).| <= |.((seq_p c1) . x).| + |.(y1 . x).| by A8, COMPLEX1:56;
A11: |.((seq_p c1) . x).| <= (seq_p c2) . x by AA7, A2, A0;
y1 . x = a1 * (x to_power k) by A2;
then |.(y1 . x).| = |.a1.| * |.(x to_power k).| by COMPLEX1:65
.= |.a1.| * (x to_power k) by ABSVALUE:def 1
.= y2 . x by A4, A5 ;
then |.((seq_p c1) . x).| + |.(y1 . x).| <= ((seq_p c2) . x) + (y2 . x) by XREAL_1:7, A11;
hence |.((seq_p c) . x).| <= (seq_p absc) . x by A9, XXREAL_0:2, A10; :: thesis: verum
end;
X1: for n being Nat holds S1[n] from NAT_1:sch 2(P0, P1);
 let c, absc be XFinSequence of REAL ; :: thesis: ( absc = |.c.| implies for n being Nat holds |.((seq_p c) . n).| <= (seq_p absc) . n )
assume X2: absc = |.c.| ; :: thesis: for n being Nat holds |.((seq_p c) . n).| <= (seq_p absc) . n
len c is Nat ;
hence for n being Nat holds |.((seq_p c) . n).| <= (seq_p absc) . n by X1, X2; :: thesis: verum