defpred S_{1}[ 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: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[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

for x being Nat holds |.((seq_p c) . x).| <= (seq_p absc) . x;

P0: S

proof

P1:
for k being Nat st S
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;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

S

proof

X1:
for n being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A0: S_{1}[k]
; :: thesis: S_{1}[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).|

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;assume A0: S

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

then AA7:
c2 = |.c1.|
by VALUED_1:def 11, A2, A4;
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;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

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

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