let n be Nat; :: thesis: for x being Element of REAL (n + 1)
for w being Element of REAL st w = x . (n + 1) holds
|.w.| <= |.x.|
let x be Element of REAL (n + 1); :: thesis: for w being Element of REAL st w = x . (n + 1) holds
|.w.| <= |.x.|
let w be Element of REAL ; :: thesis: ( w = x . (n + 1) implies |.w.| <= |.x.| )
assume A1: w = x . (n + 1) ; :: thesis: |.w.| <= |.x.|
reconsider y = x as Point of (TOP-REAL (n + 1)) by EUCLID:22;
reconsider y = y as FinSequence of REAL ;
A2: len x = n + 1 by CARD_1:def 7;
A3: n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A4: |.(y /. (n + 1)).| <= |.x.| by PDIFF_8:1;
n + 1 in dom y by A2, FINSEQ_1:def 3, A3;
hence |.w.| <= |.x.| by PARTFUN1:def 6, A4, A1; :: thesis: verum