let n be non zero Element of NAT ; :: thesis: for x being Element of (REAL-NS n)
for i being Element of NAT holds ||.((Proj (i,n)) . x).|| = |.((proj (i,n)) . x).|
let x be Element of (REAL-NS n); :: thesis: for i being Element of NAT holds ||.((Proj (i,n)) . x).|| = |.((proj (i,n)) . x).|
let i be Element of NAT ; :: thesis: ||.((Proj (i,n)) . x).|| = |.((proj (i,n)) . x).|
reconsider y = x as Element of REAL n by REAL_NS1:def 4;
(Proj (i,n)) . x = <*((proj (i,n)) . x)*> by PDIFF_1:def 4
.= <*(y . i)*> by PDIFF_1:def 1 ;
then ||.((Proj (i,n)) . x).|| = |.(y . i).| by Th2;
hence ||.((Proj (i,n)) . x).|| = |.((proj (i,n)) . x).| by PDIFF_1:def 1; :: thesis: verum