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

then A3: i in dom g by A1, GOBOARD2:3;
A4: i + 1 in dom g by A1, A2, GOBOARD2:3;
i <= (len f) + i by NAT_1:11;
then A5: 1 <= (len f) + i by A1, XXREAL_0:2;
(len f) + (i + 1) = ((len f) + i) + 1 ;
then ((len f) + i) + 1 <= (len f) + (len g) by A2, XREAL_1:8;
then A6: ((len f) + i) + 1 <= len (f ^ g) by FINSEQ_1:35;
thus LSeg g,i = LSeg (g /. i),(g /. (i + 1)) by A1, A2, TOPREAL1:def 5
.= LSeg ((f ^ g) /. ((len f) + i)),(g /. (i + 1)) by A3, FINSEQ_4:84
.= LSeg ((f ^ g) /. ((len f) + i)),((f ^ g) /. ((len f) + (i + 1))) by A4, FINSEQ_4:84
.= LSeg (f ^ g),((len f) + i) by A5, A6, TOPREAL1:def 5 ; :: 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:8;
then ((len f) + i) + 1 > len (f ^ g) by FINSEQ_1:35;
hence LSeg (f ^ g),((len f) + i) = {} by TOPREAL1:def 5
.= LSeg g,i by A7, TOPREAL1:def 5 ;
:: thesis: verum

end;

end;