let j be Element of NAT ; :: thesis: for f, g being non empty FinSequence of (TOP-REAL 2) st 1 <= j & j + 1 < len g holds
LSeg (f ^' g),((len f) + j) = LSeg g,(j + 1)
let f, g be non empty FinSequence of (TOP-REAL 2); :: thesis: ( 1 <= j & j + 1 < len g implies LSeg (f ^' g),((len f) + j) = LSeg g,(j + 1) )
assume that
A1: 1 <= j and
A2: j + 1 < len g ; :: thesis: LSeg (f ^' g),((len f) + j) = LSeg g,(j + 1)
j + 0 <= j + 1 by XREAL_1:8;
then j < len g by A2, XXREAL_0:2;
then A3: (f ^' g) /. ((len f) + j) = g /. (j + 1) by A1, GRAPH_2:62;
A4: 1 <= j + 1 by NAT_1:11;
A5: (f ^' g) /. (((len f) + j) + 1) = (f ^' g) /. ((len f) + (j + 1))
.= g /. ((j + 1) + 1) by A2, GRAPH_2:62, NAT_1:11 ;
A6: (j + 1) + 1 <= len g by A2, NAT_1:13;
j <= (len f) + j by NAT_1:11;
then A7: 1 <= (len f) + j by A1, XXREAL_0:2;
(len f) + (j + 1) < (len f) + (len g) by A2, XREAL_1:8;
then ((len f) + j) + 1 < (len (f ^' g)) + 1 by GRAPH_2:13;
then ((len f) + j) + 1 <= len (f ^' g) by NAT_1:13;
hence LSeg (f ^' g),((len f) + j) = LSeg ((f ^' g) /. ((len f) + j)),((f ^' g) /. (((len f) + j) + 1)) by A7, TOPREAL1:def 5
.= LSeg g,(j + 1) by A3, A4, A5, A6, TOPREAL1:def 5 ;
:: thesis: verum