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 that
A1: len x = len y and
A2: for i being Element of NAT st i in Seg (len x) holds
( 0 <= x . i & x . i <= y . i ) ; :: thesis: |.x.| <= |.y.|
A3: 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 A4: ( 0 <= x . i & x . i <= y . i ) by A2;
( (x . i) ^2 = (sqr x) . i & (y . i) ^2 = (sqr y) . i ) by VALUED_1:11;
hence (sqr x) . i <= (sqr y) . i by A4, SQUARE_1:15; :: thesis: verum
end;
( Seg (len (sqr y)) = dom (sqr y) & dom (sqr y) = dom y ) by FINSEQ_1:def 3, VALUED_1:11;
then A5: len (sqr y) = len y by FINSEQ_1:def 3;
( Seg (len (sqr x)) = dom (sqr x) & dom (sqr x) = dom x ) by FINSEQ_1:def 3, VALUED_1:11;
then A6: len (sqr x) = len x by FINSEQ_1:def 3;
A7: 0 <= Sum (sqr x) by RVSUM_1:86;
( 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:92;
hence |.x.| <= |.y.| by A1, A3, A6, A5, A7, RVSUM_1:82, SQUARE_1:26; :: thesis: verum