let j be Nat; :: thesis: for f, g being FinSequence of (TOP-REAL 2) st j < len f holds
LSeg ((f ^' g),j) = LSeg (f,j)
let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( j < len f implies LSeg ((f ^' g),j) = LSeg (f,j) )
assume A1: j < len f ; :: thesis: LSeg ((f ^' g),j) = LSeg (f,j)

per cases ( j < 1 or 1 <= j ) ;

suppose A2: j < 1 ; :: thesis: LSeg ((f ^' g),j) = LSeg (f,j)

hence LSeg ((f ^' g),j) = {} by TOPREAL1:def 3
.= LSeg (f,j) by A2, TOPREAL1:def 3 ;
:: thesis: verum

end;

suppose A3: 1 <= j ; :: thesis: LSeg ((f ^' g),j) = LSeg (f,j)

then A4: (f ^' g) /. j = f /. j by A1, FINSEQ_6:159;
A5: j + 1 <= len f by A1, NAT_1:13;
then A6: (f ^' g) /. (j + 1) = f /. (j + 1) by FINSEQ_6:159, NAT_1:11;
len f <= len (f ^' g) by Th7;
then j + 1 <= len (f ^' g) by A5, XXREAL_0:2;
hence LSeg ((f ^' g),j) = LSeg (((f ^' g) /. j),((f ^' g) /. (j + 1))) by A3, TOPREAL1:def 3
.= LSeg (f,j) by A3, A4, A5, A6, TOPREAL1:def 3 ;
:: thesis: verum

end;

end;