let n be Element of NAT ; :: thesis: for E being Element of REAL n

for p being FinSequence of REAL n

for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds

|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds

ex Pi being FinSequence of REAL st

( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds

|.E.| <= Sum q

let E be Element of REAL n; :: thesis: for p being FinSequence of REAL n

for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds

|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds

ex Pi being FinSequence of REAL st

( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds

|.E.| <= Sum q

let p be FinSequence of REAL n; :: thesis: for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds

|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds

ex Pi being FinSequence of REAL st

( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds

|.E.| <= Sum q

let q be FinSequence of REAL ; :: thesis: ( len p = len q & ( for j being Nat st j in dom p holds

|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds

ex Pi being FinSequence of REAL st

( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) implies |.E.| <= Sum q )

assume A1: ( len p = len q & ( for j being Nat st j in dom p holds

|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds

ex Pi being FinSequence of REAL st

( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) ) ; :: thesis: |.E.| <= Sum q

then A2: E = Sum p by Lm6;

defpred S_{1}[ Nat, set ] means ex v being Element of REAL n st

( v = p . $1 & $2 = |.v.| );

A3: for i being Nat st i in Seg (len p) holds

ex x being Element of REAL st S_{1}[i,x]

A5: ( dom u = Seg (len p) & ( for i being Nat st i in Seg (len p) holds

S_{1}[i,u . i] ) )
from FINSEQ_1:sch 5(A3);

A6: for i being Nat st i in dom p holds

ex v being Element of REAL n st

( v = p . i & u . i = |.v.| )

then A8: |.(Sum p).| <= Sum u by A6, PDIFF_6:17;

set i = len p;

reconsider uu = u as Element of (len p) -tuples_on REAL by A7, FINSEQ_2:92;

reconsider qq = q as Element of (len p) -tuples_on REAL by A1, FINSEQ_2:92;

hence |.E.| <= Sum q by A2, A8, XXREAL_0:2; :: thesis: verum

for p being FinSequence of REAL n

for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds

|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds

ex Pi being FinSequence of REAL st

( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds

|.E.| <= Sum q

let E be Element of REAL n; :: thesis: for p being FinSequence of REAL n

for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds

|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds

ex Pi being FinSequence of REAL st

( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds

|.E.| <= Sum q

let p be FinSequence of REAL n; :: thesis: for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds

|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds

ex Pi being FinSequence of REAL st

( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds

|.E.| <= Sum q

let q be FinSequence of REAL ; :: thesis: ( len p = len q & ( for j being Nat st j in dom p holds

|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds

ex Pi being FinSequence of REAL st

( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) implies |.E.| <= Sum q )

assume A1: ( len p = len q & ( for j being Nat st j in dom p holds

|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds

ex Pi being FinSequence of REAL st

( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) ) ; :: thesis: |.E.| <= Sum q

then A2: E = Sum p by Lm6;

defpred S

( v = p . $1 & $2 = |.v.| );

A3: for i being Nat st i in Seg (len p) holds

ex x being Element of REAL st S

proof

consider u being FinSequence of REAL such that
let i be Nat; :: thesis: ( i in Seg (len p) implies ex x being Element of REAL st S_{1}[i,x] )

assume i in Seg (len p) ; :: thesis: ex x being Element of REAL st S_{1}[i,x]

then A4: i in dom p by FINSEQ_1:def 3;

reconsider w = |.(p /. i).| as Element of REAL by XREAL_0:def 1;

take w ; :: thesis: S_{1}[i,w]

thus S_{1}[i,w]
by A4, PARTFUN1:def 6; :: thesis: verum

end;assume i in Seg (len p) ; :: thesis: ex x being Element of REAL st S

then A4: i in dom p by FINSEQ_1:def 3;

reconsider w = |.(p /. i).| as Element of REAL by XREAL_0:def 1;

take w ; :: thesis: S

thus S

A5: ( dom u = Seg (len p) & ( for i being Nat st i in Seg (len p) holds

S

A6: for i being Nat st i in dom p holds

ex v being Element of REAL n st

( v = p . i & u . i = |.v.| )

proof

A7:
len u = len p
by A5, FINSEQ_1:def 3;
let i be Nat; :: thesis: ( i in dom p implies ex v being Element of REAL n st

( v = p . i & u . i = |.v.| ) )

assume i in dom p ; :: thesis: ex v being Element of REAL n st

( v = p . i & u . i = |.v.| )

then i in Seg (len p) by FINSEQ_1:def 3;

hence ex v being Element of REAL n st

( v = p . i & u . i = |.v.| ) by A5; :: thesis: verum

end;( v = p . i & u . i = |.v.| ) )

assume i in dom p ; :: thesis: ex v being Element of REAL n st

( v = p . i & u . i = |.v.| )

then i in Seg (len p) by FINSEQ_1:def 3;

hence ex v being Element of REAL n st

( v = p . i & u . i = |.v.| ) by A5; :: thesis: verum

then A8: |.(Sum p).| <= Sum u by A6, PDIFF_6:17;

set i = len p;

reconsider uu = u as Element of (len p) -tuples_on REAL by A7, FINSEQ_2:92;

reconsider qq = q as Element of (len p) -tuples_on REAL by A1, FINSEQ_2:92;

now :: thesis: for j being Nat st j in Seg (len p) holds

uu . j <= qq . j

then
Sum uu <= Sum qq
by RVSUM_1:82;uu . j <= qq . j

let j be Nat; :: thesis: ( j in Seg (len p) implies uu . j <= qq . j )

assume A9: j in Seg (len p) ; :: thesis: uu . j <= qq . j

then A10: j in dom p by FINSEQ_1:def 3;

then A11: |.(p /. j).| <= q /. j by A1;

j in dom q by A9, A1, FINSEQ_1:def 3;

then A12: q /. j = q . j by PARTFUN1:def 6;

ex v being Element of REAL n st

( v = p . j & u . j = |.v.| ) by A6, A10;

hence uu . j <= qq . j by A11, A12, A10, PARTFUN1:def 6; :: thesis: verum

end;assume A9: j in Seg (len p) ; :: thesis: uu . j <= qq . j

then A10: j in dom p by FINSEQ_1:def 3;

then A11: |.(p /. j).| <= q /. j by A1;

j in dom q by A9, A1, FINSEQ_1:def 3;

then A12: q /. j = q . j by PARTFUN1:def 6;

ex v being Element of REAL n st

( v = p . j & u . j = |.v.| ) by A6, A10;

hence uu . j <= qq . j by A11, A12, A10, PARTFUN1:def 6; :: thesis: verum

hence |.E.| <= Sum q by A2, A8, XXREAL_0:2; :: thesis: verum