let f be FinSequence of (TOP-REAL 2); :: thesis: for n being Element of NAT st f is unfolded holds
f /^ n is unfolded
let n be Element of NAT ; :: thesis: ( f is unfolded implies f /^ n is unfolded )
assume A1: f is unfolded ; :: thesis: f /^ n is unfolded

per cases ( n <= len f or n > len f ) ;

suppose A2: n <= len f ; :: thesis: f /^ n is unfolded

set h = f /^ n;
let i be Nat; :: according to TOPREAL1:def 8 :: thesis: ( not 1 <= i or not i + 2 <= len (f /^ n) or (LSeg (f /^ n),i) /\ (LSeg (f /^ n),(i + 1)) = {((f /^ n) /. (i + 1))} )
assume that
A3: 1 <= i and
A4: i + 2 <= len (f /^ n) ; :: thesis: (LSeg (f /^ n),i) /\ (LSeg (f /^ n),(i + 1)) = {((f /^ n) /. (i + 1))}
A5: (i + 1) + 1 = i + (1 + 1) ;
A6: len (f /^ n) = (len f) - n by A2, RFINSEQ:def 2;
then n + (i + 2) <= len f by A4, XREAL_1:21;
then A7: (n + i) + 2 <= len f ;
A8: i + 1 in dom (f /^ n) by A3, A4, GOBOARD2:4;
i <= n + i by NAT_1:11;
then A9: 1 <= n + i by A3, XXREAL_0:2;
i + 1 <= i + 2 by XREAL_1:8;
then i + 1 <= len (f /^ n) by A4, XXREAL_0:2;
hence (LSeg (f /^ n),i) /\ (LSeg (f /^ n),(i + 1)) = (LSeg f,(n + i)) /\ (LSeg (f /^ n),(i + 1)) by A3, A6, Th5
.= (LSeg f,(n + i)) /\ (LSeg f,(n + (i + 1))) by A4, A5, A6, Th5, NAT_1:11
.= {(f /. ((n + i) + 1))} by A1, A7, A9, TOPREAL1:def 8
.= {(f /. (n + (i + 1)))}
.= {((f /^ n) /. (i + 1))} by A8, FINSEQ_5:30 ;
:: thesis: verum

end;

suppose n > len f ; :: thesis: f /^ n is unfolded

then f /^ n = <*> the carrier of (TOP-REAL 2) by RFINSEQ:def 2;
then len (f /^ n) = 0 ;
hence f /^ n is unfolded by Th27; :: thesis: verum

end;

end;