let f be FinSequence of (TOP-REAL 2); for n being Nat st f is unfolded holds
f | n is unfolded
let n be Nat; ( f is unfolded implies f | n is unfolded )
assume A1:
f is unfolded
; f | n is unfolded
set h = f | n;
let i be Nat; TOPREAL1:def 6 ( 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)
; (LSeg ((f | n),i)) /\ (LSeg ((f | n),(i + 1))) = {((f | n) /. (i + 1))}
A4:
i + 1 in dom (f | n)
by A2, A3, SEQ_4:135;
len (f | n) <= len f
by FINSEQ_5:16;
then A5:
i + 2 <= len f
by A3, XXREAL_0:2;
A6:
(i + 1) + 1 = i + (1 + 1)
;
i + 1 <= i + 2
by XREAL_1:6;
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, A6, Th3
.=
{(f /. (i + 1))}
by A1, A2, A5
.=
{((f | n) /. (i + 1))}
by A4, FINSEQ_4:70
;
verum