let i be Nat; :: thesis: for D being non empty set
for f, g being FinSequence of D holds (f ^ g) /^ ((len f) + i) = g /^ i
let D be non empty set ; :: thesis: for f, g being FinSequence of D holds (f ^ g) /^ ((len f) + i) = g /^ i
let f, g be FinSequence of D; :: thesis: (f ^ g) /^ ((len f) + i) = g /^ i
A1: len (f ^ g) = (len f) + (len g) by FINSEQ_1:35;

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:8;
then A3: len ((f ^ g) /^ ((len f) + i)) = ((len g) + (len f)) - ((len f) + i) by A1, RFINSEQ:def 2
.= (len g) - i
.= len (g /^ i) by A2, RFINSEQ:def 2 ;

now

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:27;
then A6: i + k in dom g by Th29;
k in dom ((f ^ g) /^ ((len f) + i)) by A3, A4, FINSEQ_3:27;
hence ((f ^ g) /^ ((len f) + i)) /. k = (f ^ g) /. (((len f) + i) + k) by Th30
.= (f ^ g) /. ((len f) + (i + k))
.= g /. (i + k) by A6, FINSEQ_4:84
.= (g /^ i) /. k by A5, Th30 ;
:: thesis: verum

end;

hence (f ^ g) /^ ((len f) + i) = g /^ i by A3, Th14; :: 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:8;
hence (f ^ g) /^ ((len f) + i) = <*> D by RFINSEQ:def 2
.= g /^ i by A7, RFINSEQ:def 2 ;
:: thesis: verum

end;

end;