let Y be RealNormSpace; :: thesis: for p being FinSequence of Y
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 ) holds
||.(Sum p).|| <= Sum q
let p be FinSequence of Y; :: 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 ) holds
||.(Sum p).|| <= 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 ) 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 Point of Y 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 ;
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 Point of Y st
( v = p /. i & u . i = ||.v.|| )

proof

let i be Element of NAT ; :: thesis: ( i in dom p implies ex v being Point of Y st
( v = p /. i & u . i = ||.v.|| ) )
assume i in dom p ; :: thesis: ex v being Point of Y st
( v = p /. i & u . i = ||.v.|| )
then i in Seg (len p) by FINSEQ_1:def 3;
hence ex v being Point of Y 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, Th9;
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 Point of Y st
( v = p /. j & u . j = ||.v.|| ) by A4;
hence uu . j <= qq . j by A7, A1; :: thesis: verum

end;

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