let n be non zero Element of NAT ; :: thesis: for i being Nat holds (proj (i,n)) . (0. (REAL-NS n)) = 0
let i be Nat; :: thesis: (proj (i,n)) . (0. (REAL-NS n)) = 0
thus (proj (i,n)) . (0. (REAL-NS n)) = (proj (i,n)) . (0* n) by REAL_NS1:def 4
.= (0* n) . i by PDIFF_1:def 1
.= 0 ; :: thesis: verum