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

A2: now :: thesis: for x being Element of REAL n holds
( (h * (proj (i,n))) . x = <*((proj (i,n)) . x)*> & (Proj (i,n)) . x = (h * (proj (i,n))) . x )

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;
A3: (h * (proj (i,n))) . x = h . ((proj (i,n)) . x) by FUNCT_2:15;
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 A3, Lm1; :: thesis: verum

end;

the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;
hence Proj (i,n) = ((proj (1,1)) ") * (proj (i,n)) by A1, A2, FUNCT_2:63; :: thesis: verum