let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds |(p,(0. (TOP-REAL n)))| = 0

let p be Point of (TOP-REAL n); :: thesis: |(p,(0. (TOP-REAL n)))| = 0

reconsider f1 = p as FinSequence of REAL by EUCLID:24;

len f1 = n by CARD_1:def 7;

then 0* (len f1) = 0. (TOP-REAL n) by EUCLID:70;

hence |(p,(0. (TOP-REAL n)))| = 0 by Th8; :: thesis: verum

let p be Point of (TOP-REAL n); :: thesis: |(p,(0. (TOP-REAL n)))| = 0

reconsider f1 = p as FinSequence of REAL by EUCLID:24;

len f1 = n by CARD_1:def 7;

then 0* (len f1) = 0. (TOP-REAL n) by EUCLID:70;

hence |(p,(0. (TOP-REAL n)))| = 0 by Th8; :: thesis: verum