let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds |(p,(0.REAL n))| = 0
let p be Point of (TOP-REAL n); :: thesis: |(p,(0.REAL n))| = 0
reconsider f1 = p as FinSequence of REAL by EUCLID:27;
len f1 = n by EUCLID:28;
hence |(p,(0.REAL n))| = 0 by Th17; :: thesis: verum