let f be FinSequence of (TOP-REAL 2); :: thesis: for j, i being Element of NAT st j in dom (f | i) & j + 1 in dom (f | i) holds
LSeg f,j = LSeg (f | i),j
let j, i be Element of 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:27;
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:90;
then j in dom f by XBOOLE_0:def 4;
then A5: 1 <= j by FINSEQ_3:27;
j + 1 in (dom f) /\ (Seg i) by A2, A4, RELAT_1:90;
then j + 1 in dom f by XBOOLE_0:def 4;
then A6: j + 1 <= len f by FINSEQ_3:27;
( (f | i) /. j = f /. j & (f | i) /. (j + 1) = f /. (j + 1) ) by A1, A2, FINSEQ_4:85;
then LSeg f,j = LSeg ((f | i) /. j),((f | i) /. (j + 1)) by A5, A6, TOPREAL1:def 5;
hence LSeg f,j = LSeg (f | i),j by A3, TOPREAL1:def 5; :: thesis: verum