let f, g be FinSequence of (TOP-REAL 2); :: thesis: for i being Nat st i + 1 <= len f holds
LSeg ((f ^ g),i) = LSeg (f,i)
let i be Nat; :: thesis: ( i + 1 <= len f implies LSeg ((f ^ g),i) = LSeg (f,i) )
assume A1: i + 1 <= len f ; :: thesis: LSeg ((f ^ g),i) = LSeg (f,i)

per cases ( i <> 0 or i = 0 ) ;

suppose i <> 0 ; :: thesis: LSeg ((f ^ g),i) = LSeg (f,i)

then A2: 1 <= i by NAT_1:14;
then A3: i in dom f by A1, SEQ_4:134;
len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then len (f ^ g) >= len f by NAT_1:11;
then A4: i + 1 <= len (f ^ g) by A1, XXREAL_0:2;
A5: i + 1 in dom f by A1, A2, SEQ_4:134;
thus LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A1, A2, TOPREAL1:def 3
.= LSeg (((f ^ g) /. i),(f /. (i + 1))) by A3, FINSEQ_4:68
.= LSeg (((f ^ g) /. i),((f ^ g) /. (i + 1))) by A5, FINSEQ_4:68
.= LSeg ((f ^ g),i) by A2, A4, TOPREAL1:def 3 ; :: thesis: verum

end;

suppose A6: i = 0 ; :: thesis: LSeg ((f ^ g),i) = LSeg (f,i)

hence LSeg ((f ^ g),i) = {} by TOPREAL1:def 3
.= LSeg (f,i) by A6, TOPREAL1:def 3 ;
:: thesis: verum

end;

end;