let n be Nat; :: thesis: for p being Point of holds p is Function of Seg n, REAL
let p be Point of ; :: thesis: p is Function of Seg n, REAL
TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by Def8;
then p is Element of Funcs (Seg n),REAL by FINSEQ_2:111;
hence p is Function of Seg n, REAL ; :: thesis: verum