let f, h be FinSequence of (TOP-REAL 2); 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; ( 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
; 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; verum