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 A1: ( j in dom f & j + 1 in dom f ) ; :: thesis: LSeg (f ^ h),j = LSeg f,j
set p1 = f /. j;
set p2 = f /. (j + 1);
A2: f /. j = (f ^ h) /. j by A1, FINSEQ_4:83;
A3: f /. (j + 1) = (f ^ h) /. (j + 1) by A1, FINSEQ_4:83;
dom f c= dom (f ^ h) by FINSEQ_1:39;
then ( 1 <= j & j + 1 <= len (f ^ h) ) by A1, FINSEQ_3:27;
then A4: LSeg (f ^ h),j = LSeg (f /. j),(f /. (j + 1)) by A2, A3, TOPREAL1:def 5;
( 1 <= j & j + 1 <= len f ) by A1, FINSEQ_3:27;
hence LSeg (f ^ h),j = LSeg f,j by A4, TOPREAL1:def 5; :: thesis: verum