let f be FinSequence of ; :: thesis: for p being Point of st p in rng f & f is unfolded holds
f :- p is unfolded
let p be Point of ; :: thesis: ( p in rng f & f is unfolded implies f :- p is unfolded )
assume p in rng f ; :: thesis: ( not f is unfolded or f :- p is unfolded )
then ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i ) by FINSEQ_5:52;
hence ( not f is unfolded or f :- p is unfolded ) ; :: thesis: verum