let j be 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))
A3: (f ^' g) /. (((len f) + j) + 1) = (f ^' g) /. ((len f) + (j + 1))
.= g /. ((j + 1) + 1) by A2, FINSEQ_6:160, NAT_1:11 ;
j + 0 <= j + 1 by XREAL_1:6;
then j < len g by A2, XXREAL_0:2;
then A4: (f ^' g) /. ((len f) + j) = g /. (j + 1) by A1, FINSEQ_6:160;
A5: 1 <= j + 1 by NAT_1:11;
(len f) + (j + 1) < (len f) + (len g) by A2, XREAL_1:6;
then ((len f) + j) + 1 < (len (f ^' g)) + 1 by FINSEQ_6:139;
then A6: ((len f) + j) + 1 <= len (f ^' g) by NAT_1:13;
A7: (j + 1) + 1 <= len g by A2, NAT_1:13;
j <= (len f) + j by NAT_1:11;
then 1 <= (len f) + j by A1, XXREAL_0:2;
hence LSeg ((f ^' g),((len f) + j)) = LSeg (((f ^' g) /. ((len f) + j)),((f ^' g) /. (((len f) + j) + 1))) by A6, TOPREAL1:def 3
.= LSeg (g,(j + 1)) by A4, A5, A3, A7, TOPREAL1:def 3 ;
:: thesis: verum