let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds p is Function of (Seg n),REAL
let p be Point of (TOP-REAL n); :: 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