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
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
A2: 1 <= i and
A3: i + 2 <= len (f | n) ; :: thesis: (LSeg (f | n),i) /\ (LSeg (f | n),(i + 1)) = {((f | n) /. (i + 1))}
A4: (i + 1) + 1 = i + (1 + 1) ;
len (f | n) <= len f by FINSEQ_5:18;
then A5: i + 2 <= len f by A3, XXREAL_0:2;
A6: i + 1 in dom (f | n) by A2, A3, GOBOARD2:4;
i + 1 <= i + 2 by XREAL_1:8;
hence (LSeg (f | n),i) /\ (LSeg (f | n),(i + 1)) = (LSeg f,i) /\ (LSeg (f | n),(i + 1)) by A3, Th3, XXREAL_0:2
.= (LSeg f,i) /\ (LSeg f,(i + 1)) by A3, A4, Th3
.= {(f /. (i + 1))} by A1, A2, A5, TOPREAL1:def 8
.= {((f | n) /. (i + 1))} by A6, FINSEQ_4:85 ;
:: thesis: verum