let n be Nat; :: thesis: for x being Point of (REAL-NS n)
for y being Element of REAL n st x = y holds
for i being Nat st i in Seg n holds
|.(y . i).| <= ||.x.||
let x be Point of (REAL-NS n); :: thesis: for y being Element of REAL n st x = y holds
for i being Nat st i in Seg n holds
|.(y . i).| <= ||.x.||
let y be Element of REAL n; :: thesis: ( x = y implies for i being Nat st i in Seg n holds
|.(y . i).| <= ||.x.|| )
assume x = y ; :: thesis: for i being Nat st i in Seg n holds
|.(y . i).| <= ||.x.||
then ||.x.|| = |.y.| by Th1;
hence for i being Nat st i in Seg n holds
|.(y . i).| <= ||.x.|| by Th8; :: thesis: verum