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

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