let i, k be Nat; :: thesis: for D being non empty set
for f being FinSequence of D holds f /^ (i + k) = (f /^ i) /^ k
let D be non empty set ; :: thesis: for f being FinSequence of D holds f /^ (i + k) = (f /^ i) /^ k
let f be FinSequence of D; :: thesis: f /^ (i + k) = (f /^ i) /^ k

per cases ( i + k <= len f or ( i + k > len f & i <= len f ) or ( i + k > len f & i > len f ) ) ;

suppose A1: i + k <= len f ; :: thesis: f /^ (i + k) = (f /^ i) /^ k

i <= i + k by NAT_1:11;
then A2: i <= len f by A1, XXREAL_0:2;
then A3: len (f /^ i) = (len f) - i by RFINSEQ:def 1;
then A4: k <= len (f /^ i) by A1, XREAL_1:19;

A5: now :: thesis: for m being Nat st m in dom ((f /^ i) /^ k) holds
((f /^ i) /^ k) . m = f . (m + (i + k))

let m be Nat; :: thesis: ( m in dom ((f /^ i) /^ k) implies ((f /^ i) /^ k) . m = f . (m + (i + k)) )
assume A6: m in dom ((f /^ i) /^ k) ; :: thesis: ((f /^ i) /^ k) . m = f . (m + (i + k))
then A7: m + k in dom (f /^ i) by FINSEQ_5:26;
thus ((f /^ i) /^ k) . m = (f /^ i) . (m + k) by A4, A6, RFINSEQ:def 1
.= f . ((m + k) + i) by A2, A7, RFINSEQ:def 1
.= f . (m + (i + k)) ; :: thesis: verum

end;

len ((f /^ i) /^ k) = (len (f /^ i)) - k by A4, RFINSEQ:def 1
.= (len f) - (i + k) by A3 ;
hence f /^ (i + k) = (f /^ i) /^ k by A1, A5, RFINSEQ:def 1; :: thesis: verum

end;

suppose that A8: i + k > len f and
A9: i <= len f ; :: thesis: f /^ (i + k) = (f /^ i) /^ k

len (f /^ i) = (len f) - i by A9, RFINSEQ:def 1;
then (len (f /^ i)) + i = len f ;
then A10: k > len (f /^ i) by A8, XREAL_1:6;
thus f /^ (i + k) = <*> D by A8, RFINSEQ:def 1
.= (f /^ i) /^ k by A10, RFINSEQ:def 1 ; :: thesis: verum

end;

suppose that A11: i + k > len f and
A12: i > len f ; :: thesis: f /^ (i + k) = (f /^ i) /^ k

thus f /^ (i + k) = <*> D by A11, RFINSEQ:def 1
.= (<*> D) /^ k by Th80
.= (f /^ i) /^ k by A12, RFINSEQ:def 1 ; :: thesis: verum

end;

end;