let f, h be FinSequence of (TOP-REAL 2); :: thesis: for j being Nat st j in dom f & j + 1 in dom f holds
LSeg ((f ^ h),j) = LSeg (f,j)
let j be 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:25;
dom f c= dom (f ^ h) by FINSEQ_1:26;
then A4: j + 1 <= len (f ^ h) by A2, FINSEQ_3:25;
set p1 = f /. j;
set p2 = f /. (j + 1);
A5: 1 <= j by A1, FINSEQ_3:25;
( f /. j = (f ^ h) /. j & f /. (j + 1) = (f ^ h) /. (j + 1) ) by A1, A2, FINSEQ_4:68;
then LSeg ((f ^ h),j) = LSeg ((f /. j),(f /. (j + 1))) by A5, A4, TOPREAL1:def 3;
hence LSeg ((f ^ h),j) = LSeg (f,j) by A3, TOPREAL1:def 3; :: thesis: verum