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₁[ 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₁[i,x]

proof

let i be Nat; :: thesis: ( i in Seg (len p) implies ex x being Element of REAL st S₁[i,x] )
assume i in Seg (len p) ; :: thesis: ex x being Element of REAL st S₁[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₁[i,w]
thus S₁[i,w] by A4, PARTFUN1:def 6; :: thesis: verum

end;

consider u being FinSequence of REAL such that
A5: ( dom u = Seg (len p) & ( for i being Nat st i in Seg (len p) holds
S₁[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.| )

proof

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;

A7: len u = len p by A5, FINSEQ_1:def 3;
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

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;

then Sum uu <= Sum qq by RVSUM_1:82;
hence |.E.| <= Sum q by A2, A8, XXREAL_0:2; :: thesis: verum