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

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