let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds p is FinSequence of REAL
let p be Point of (TOP-REAL n); :: thesis: p is FinSequence of REAL
p is Function of (Seg n),REAL by Th20;
hence p is FinSequence of REAL by FINSEQ_2:25; :: thesis: verum