let j be Element of NAT ; :: thesis: for f being non empty FinSequence of (TOP-REAL 2)
for g being non trivial FinSequence of (TOP-REAL 2) st j + 1 < len g & f /. (len f) = g /. 1 holds
LSeg (f ^' g),((len f) + j) = LSeg g,(j + 1)
let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for g being non trivial FinSequence of (TOP-REAL 2) st j + 1 < len g & f /. (len f) = g /. 1 holds
LSeg (f ^' g),((len f) + j) = LSeg g,(j + 1)
let g be non trivial FinSequence of (TOP-REAL 2); :: thesis: ( j + 1 < len g & f /. (len f) = g /. 1 implies LSeg (f ^' g),((len f) + j) = LSeg g,(j + 1) )
assume that
A1: j + 1 < len g and
A2: f /. (len f) = g /. 1 ; :: thesis: LSeg (f ^' g),((len f) + j) = LSeg g,(j + 1)

per cases ( j = 0 or 1 <= j ) by NAT_1:14;

suppose j = 0 ; :: thesis: LSeg (f ^' g),((len f) + j) = LSeg g,(j + 1)

hence LSeg (f ^' g),((len f) + j) = LSeg g,(j + 1) by A2, Th30; :: thesis: verum

end;

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

hence LSeg (f ^' g),((len f) + j) = LSeg g,(j + 1) by A1, Th29; :: thesis: verum

end;

end;