let f be FinSequence of (TOP-REAL 2); :: thesis: for n being Nat st f is unfolded holds

f /^ n is unfolded

let n be Nat; :: thesis: ( f is unfolded implies f /^ n is unfolded )

assume A1: f is unfolded ; :: thesis: f /^ n is unfolded

f /^ n is unfolded

let n be 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 )
;

end;

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

set h = f /^ n;

let i be Nat; :: according to TOPREAL1:def 6 :: 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 in dom (f /^ n) by A3, A4, SEQ_4:135;

A6: len (f /^ n) = (len f) - n by A2, RFINSEQ:def 1;

then n + (i + 2) <= len f by A4, XREAL_1:19;

then A7: (n + i) + 2 <= len f ;

i <= n + i by NAT_1:11;

then A8: 1 <= n + i by A3, XXREAL_0:2;

A9: (i + 1) + 1 = i + (1 + 1) ;

i + 1 <= i + 2 by XREAL_1:6;

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, A9, A6, Th5, NAT_1:11

.= {(f /. ((n + i) + 1))} by A1, A7, A8

.= {(f /. (n + (i + 1)))}

.= {((f /^ n) /. (i + 1))} by A5, FINSEQ_5:27 ;

:: thesis: verum

end;let i be Nat; :: according to TOPREAL1:def 6 :: 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 in dom (f /^ n) by A3, A4, SEQ_4:135;

A6: len (f /^ n) = (len f) - n by A2, RFINSEQ:def 1;

then n + (i + 2) <= len f by A4, XREAL_1:19;

then A7: (n + i) + 2 <= len f ;

i <= n + i by NAT_1:11;

then A8: 1 <= n + i by A3, XXREAL_0:2;

A9: (i + 1) + 1 = i + (1 + 1) ;

i + 1 <= i + 2 by XREAL_1:6;

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, A9, A6, Th5, NAT_1:11

.= {(f /. ((n + i) + 1))} by A1, A7, A8

.= {(f /. (n + (i + 1)))}

.= {((f /^ n) /. (i + 1))} by A5, FINSEQ_5:27 ;

:: thesis: verum