let j be 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;