let p, q, r be FinSequence; :: thesis: for k being Nat st len p < k & k <= len (p ^ q) holds
((p ^ q) ^ r) . k = q . (k - (len p))
let k be Nat; :: thesis: ( len p < k & k <= len (p ^ q) implies ((p ^ q) ^ r) . k = q . (k - (len p)) )
assume that
A1: len p < k and
A2: k <= len (p ^ q) ; :: thesis: ((p ^ q) ^ r) . k = q . (k - (len p))
len (p ^ q) <= len (p ^ (q ^ r)) by Th11;
then k <= len (p ^ (q ^ r)) by A2, XXREAL_0:2;
then A3: (p ^ (q ^ r)) . k = (q ^ r) . (k - (len p)) by A1, FINSEQ_1:37;
set n = k - (len p);
(len p) - (len p) = 0 ;
then A4: 0 < k - (len p) by A1, XREAL_1:11;
0 + 1 = 1 ;
then A5: 1 <= k - (len p) by A4, INT_1:20;
then reconsider n = k - (len p) as Nat by Th3;
A6: k <= (len p) + (len q) by A2, FINSEQ_1:35;
n <= len q

proof

((len p) + (len q)) - (len p) = len q ;
hence n <= len q by A6, XREAL_1:11; :: thesis: verum

end;

then n in Seg (len q) by A5, FINSEQ_1:3;
then A7: n in dom q by FINSEQ_1:def 3;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
(q ^ r) . n = q . n by A7, FINSEQ_1:def 7;
hence ((p ^ q) ^ r) . k = q . (k - (len p)) by A3, FINSEQ_1:45; :: thesis: verum