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:93;
hence p is Function of (Seg n),REAL ; :: thesis: verum