let n be non zero Element of NAT ; :: thesis: for x being Element of REAL n
for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . x).| <= |.x.|
let x be Element of REAL n; :: thesis: for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . x).| <= |.x.|
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= n implies |.((proj (i,n)) . x).| <= |.x.| )
assume A1: ( 1 <= i & i <= n ) ; :: thesis: |.((proj (i,n)) . x).| <= |.x.|
reconsider y = x as Element of (REAL-NS n) by REAL_NS1:def 4;
A2: ||.((Proj (i,n)) . y).|| = |.((proj (i,n)) . y).| by Th4;
||.((Proj (i,n)) . y).|| <= ||.y.|| by A1, Th3;
hence |.((proj (i,n)) . x).| <= |.x.| by A2, REAL_NS1:1; :: thesis: verum