let x, y be FinSequence of REAL ; :: thesis: ( len x = len y & ( for i being Element of NAT st i in Seg (len x) holds
( 0 <= x . i & x . i <= y . i ) ) implies |.x.| <= |.y.| )
assume A1: ( len x = len y & ( for i being Element of NAT st i in Seg (len x) holds
( 0 <= x . i & x . i <= y . i ) ) ) ; :: thesis: |.x.| <= |.y.|
A2: for i being Nat st i in Seg (len x) holds
(sqr x) . i <= (sqr y) . i

proof

let i be Nat; :: thesis: ( i in Seg (len x) implies (sqr x) . i <= (sqr y) . i )
assume i in Seg (len x) ; :: thesis: (sqr x) . i <= (sqr y) . i
then A3: ( 0 <= x . i & x . i <= y . i ) by A1;
( (x . i) ^2 = (sqr x) . i & (y . i) ^2 = (sqr y) . i ) by VALUED_1:11;
hence (sqr x) . i <= (sqr y) . i by A3, SQUARE_1:77; :: thesis: verum

end;

A4: ( Seg (len (sqr x)) = dom (sqr x) & Seg (len (sqr y)) = dom (sqr y) ) by FINSEQ_1:def 3;
( dom (sqr x) = dom x & dom (sqr y) = dom y ) by VALUED_1:11;
then A5: ( len (sqr x) = len x & len (sqr y) = len y ) by A4, FINSEQ_1:def 3;
( sqr x is Element of (len (sqr x)) -tuples_on REAL & sqr y is Element of (len (sqr y)) -tuples_on REAL ) by FINSEQ_2:110;
then A6: Sum (sqr x) <= Sum (sqr y) by A1, A2, A5, RVSUM_1:112;
0 <= Sum (sqr x) by RVSUM_1:116;
hence |.x.| <= |.y.| by A6, SQUARE_1:94; :: thesis: verum