let j be Element of 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 5
.= LSeg f,j by A2, TOPREAL1:def 5 ;
:: thesis: verum

end;

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

then A4: (f ^' g) /. j = f /. j by A1, GRAPH_2:61;
A5: j + 1 <= len f by A1, NAT_1:13;
then A6: (f ^' g) /. (j + 1) = f /. (j + 1) by GRAPH_2:61, 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 5
.= LSeg f,j by A3, A4, A5, A6, TOPREAL1:def 5 ;
:: thesis: verum

end;

end;