let n be Nat; :: thesis: for p being Point of holds p is FinSequence of REAL
let p be Point of ; :: thesis: p is FinSequence of REAL
p is Function of Seg n, REAL by Th26;
hence p is FinSequence of REAL by FINSEQ_2:28; :: thesis: verum