let f, h be FinSequence of (TOP-REAL 2); :: thesis: for j being Element of NAT st j in dom f & j + 1 in dom f holds
LSeg (f ^ h),j = LSeg f,j
let j be Element of NAT ; :: thesis: ( j in dom f & j + 1 in dom f implies LSeg (f ^ h),j = LSeg f,j )
assume that
A1: j in dom f and
A2: j + 1 in dom f ; :: thesis: LSeg (f ^ h),j = LSeg f,j
A3: ( 1 <= j & j + 1 <= len f ) by A1, A2, FINSEQ_3:27;
dom f c= dom (f ^ h) by FINSEQ_1:39;
then A4: j + 1 <= len (f ^ h) by A2, FINSEQ_3:27;
set p1 = f /. j;
set p2 = f /. (j + 1);
A5: 1 <= j by A1, FINSEQ_3:27;
( f /. j = (f ^ h) /. j & f /. (j + 1) = (f ^ h) /. (j + 1) ) by A1, A2, FINSEQ_4:83;
then LSeg (f ^ h),j = LSeg (f /. j),(f /. (j + 1)) by A5, A4, TOPREAL1:def 5;
hence LSeg (f ^ h),j = LSeg f,j by A3, TOPREAL1:def 5; :: thesis: verum