let p, q be FinSequence of REAL ; :: thesis: ( len p = len q & ( for j being Nat st j in dom p holds
|.(p . j).| <= q . j ) implies |.(Sum p).| <= Sum q )
assume A1: ( len p = len q & ( for j being Nat st j in dom p holds
|.(p . j).| <= q . j ) ) ; :: thesis: |.(Sum p).| <= Sum q
defpred S₁[ Nat, set ] means ex v being Real st
( v = p . $1 & $2 = |.v.| );
A2: 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]
reconsider w = |.(p . i).| as Element of REAL by XREAL_0:def 1;
take w ; :: thesis: S₁[i,w]
thus S₁[i,w] ; :: thesis: verum

end;

consider u being FinSequence of REAL such that
A3: ( 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(A2);
A4: for i being Element of NAT st i in dom p holds
ex v being Real st
( v = p . i & u . i = |.v.| )

proof

let i be Element of NAT ; :: thesis: ( i in dom p implies ex v being Real st
( v = p . i & u . i = |.v.| ) )
assume i in dom p ; :: thesis: ex v being Real st
( v = p . i & u . i = |.v.| )
then i in Seg (len p) by FINSEQ_1:def 3;
hence ex v being Real st
( v = p . i & u . i = |.v.| ) by A3; :: thesis: verum

end;

A5: len u = len p by A3, FINSEQ_1:def 3;
then A6: |.(Sum p).| <= Sum u by A4, Th2;
set i = len p;
reconsider uu = u as Element of (len p) -tuples_on REAL by A5, 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 j in Seg (len p) ; :: thesis: uu . j <= qq . j
then A7: j in dom p by FINSEQ_1:def 3;
then ex v being Real st
( v = p . j & u . j = |.v.| ) by A4;
hence uu . j <= qq . j by A1, A7; :: thesis: verum

end;

then Sum uu <= Sum qq by RVSUM_1:82;
hence |.(Sum p).| <= Sum q by A6, XXREAL_0:2; :: thesis: verum