let i be Nat; :: thesis: for f, g being FinSequence holds (f ^ g) /^ ((len f) + i) = g /^ i
let f, g be FinSequence; :: thesis: (f ^ g) /^ ((len f) + i) = g /^ i
A1: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;

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

suppose A2: i <= len g ; :: thesis: (f ^ g) /^ ((len f) + i) = g /^ i

then (len f) + i <= (len f) + (len g) by XREAL_1:6;
then A3: len ((f ^ g) /^ ((len f) + i)) = ((len g) + (len f)) - ((len f) + i) by A1, RFINSEQ:def 1
.= (len g) - i
.= len (g /^ i) by A2, RFINSEQ:def 1 ;

now :: thesis: for k being Nat st 1 <= k & k <= len (g /^ i) holds
((f ^ g) /^ ((len f) + i)) . k = (g /^ i) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len (g /^ i) implies ((f ^ g) /^ ((len f) + i)) . k = (g /^ i) . k )
assume A4: ( 1 <= k & k <= len (g /^ i) ) ; :: thesis: ((f ^ g) /^ ((len f) + i)) . k = (g /^ i) . k
then A5: k in dom (g /^ i) by FINSEQ_3:25;
then A6: i + k in dom g by Th26;
k in dom ((f ^ g) /^ ((len f) + i)) by A3, A4, FINSEQ_3:25;
hence ((f ^ g) /^ ((len f) + i)) . k = (f ^ g) . (((len f) + i) + k) by Th27
.= (f ^ g) . ((len f) + (i + k))
.= g . (i + k) by A6, FINSEQ_1:def 7
.= (g /^ i) . k by A5, Th27 ;
:: thesis: verum

end;

hence (f ^ g) /^ ((len f) + i) = g /^ i by A3; :: thesis: verum

end;

suppose A7: i > len g ; :: thesis: (f ^ g) /^ ((len f) + i) = g /^ i

then (len f) + i > len (f ^ g) by A1, XREAL_1:6;
hence (f ^ g) /^ ((len f) + i) = {} by RFINSEQ:def 1
.= g /^ i by A7, RFINSEQ:def 1 ;
:: thesis: verum

end;

end;