let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is unfolded holds
f -: p is unfolded
let p be Point of (TOP-REAL 2); :: thesis: ( f is unfolded implies f -: p is unfolded )
f -: p = f | (p .. f) by FINSEQ_5:def 1;
hence ( f is unfolded implies f -: p is unfolded ) ; :: thesis: verum