let n be non empty Element of NAT ; :: thesis: for i being Element of NAT holds Proj i,n = ((proj 1,1) " ) * (proj i,n)
let i be Element of NAT ; :: thesis: Proj i,n = ((proj 1,1) " ) * (proj i,n)
A1: ( the carrier of (REAL-NS 1) = REAL 1 & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
reconsider h = (proj 1,1) " as Function of REAL ,(REAL 1) by Th2;

now

let x be Element of REAL n; :: thesis: ( (h * (proj i,n)) . x = <*((proj i,n) . x)*> & (Proj i,n) . x = (h * (proj i,n)) . x )
reconsider z = x as Point of (REAL-NS n) by REAL_NS1:def 4;
A2: (h * (proj i,n)) . x = h . ((proj i,n) . x) by FUNCT_2:21;
hence (h * (proj i,n)) . x = <*((proj i,n) . x)*> by Lm1; :: thesis: (Proj i,n) . x = (h * (proj i,n)) . x
(Proj i,n) . x = (Proj i,n) . z ;
then (Proj i,n) . x = <*((proj i,n) . x)*> by Def4;
hence (Proj i,n) . x = (h * (proj i,n)) . x by A2, Lm1; :: thesis: verum

end;

hence Proj i,n = ((proj 1,1) " ) * (proj i,n) by A1, FUNCT_2:113; :: thesis: verum