let f be FinSequence of (TOP-REAL 2); :: thesis: for i, j being Nat st j in dom (f | i) & j + 1 in dom (f | i) holds
LSeg (f,j) = LSeg ((f | i),j)
let i, j be Nat; :: thesis: ( j in dom (f | i) & j + 1 in dom (f | i) implies LSeg (f,j) = LSeg ((f | i),j) )
assume that
A1: j in dom (f | i) and
A2: j + 1 in dom (f | i) ; :: thesis: LSeg (f,j) = LSeg ((f | i),j)
A3: ( 1 <= j & j + 1 <= len (f | i) ) by A1, A2, FINSEQ_3:25;
set p1 = (f | i) /. j;
set p2 = (f | i) /. (j + 1);
A4: f | i = f | (Seg i) by FINSEQ_1:def 15;
then j in (dom f) /\ (Seg i) by A1, RELAT_1:61;
then j in dom f by XBOOLE_0:def 4;
then A5: 1 <= j by FINSEQ_3:25;
j + 1 in (dom f) /\ (Seg i) by A2, A4, RELAT_1:61;
then j + 1 in dom f by XBOOLE_0:def 4;
then A6: j + 1 <= len f by FINSEQ_3:25;
( (f | i) /. j = f /. j & (f | i) /. (j + 1) = f /. (j + 1) ) by A1, A2, FINSEQ_4:70;
then LSeg (f,j) = LSeg (((f | i) /. j),((f | i) /. (j + 1))) by A5, A6, TOPREAL1:def 3;
hence LSeg (f,j) = LSeg ((f | i),j) by A3, TOPREAL1:def 3; :: thesis: verum