let n be Nat; :: thesis: for f being n -element real-valued FinSequence holds f is Point of (TOP-REAL n)
let f be n -element real-valued FinSequence; :: thesis: f is Point of (TOP-REAL n)
( len f = n & @ (@ f) = f ) by CARD_1:def 7;
hence f is Point of (TOP-REAL n) by TOPREAL3:46; :: thesis: verum