let n be non zero Element of NAT ; :: thesis: for i being Element of NAT holds Proj (i,n) is homogeneous
let i be Element of NAT ; :: thesis: Proj (i,n) is homogeneous
thus for x being Point of (REAL-NS n)
for r being Real holds (Proj (i,n)) . (r * x) = r * ((Proj (i,n)) . x) by PDIFF_6:27; :: according to LOPBAN_1:def 5 :: thesis: verum