let n be non zero Nat; for i being Nat holds Proj (i,n) = ((proj (1,1)) ") * (proj (i,n))
let i be Nat; 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 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;
( (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;
(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;
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; verum