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

per cases ( i + 1 <= len g or i + 1 > len g ) ;

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

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

end;

suppose A7: i + 1 > len g ; :: thesis: LSeg ((f ^ g),((len f) + i)) = LSeg (g,i)

then (len f) + (i + 1) > (len f) + (len g) by XREAL_1:6;
then ((len f) + i) + 1 > len (f ^ g) by FINSEQ_1:22;
hence LSeg ((f ^ g),((len f) + i)) = {} by TOPREAL1:def 3
.= LSeg (g,i) by A7, TOPREAL1:def 3 ;
:: thesis: verum

end;

end;