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))
set n = k - (len p);
(len p) - (len p) = 0 ;
then A3: 0 < k - (len p) by A1, XREAL_1:9;
0 + 1 = 1 ;
then A4: 1 <= k - (len p) by A3, INT_1:7;
then reconsider n = k - (len p) as Nat by Th2;
A5: ((len p) + (len q)) - (len p) = len q ;
k <= (len p) + (len q) by A2, FINSEQ_1:22;
then n <= len q by A5, XREAL_1:9;
then n in Seg (len q) by A4;
then A6: n in dom q by FINSEQ_1:def 3;
len (p ^ q) <= len (p ^ (q ^ r)) by Th9;
then k <= len (p ^ (q ^ r)) by A2, XXREAL_0:2;
then A7: (p ^ (q ^ r)) . k = (q ^ r) . (k - (len p)) by A1, FINSEQ_1:24;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
(q ^ r) . n = q . n by A6, FINSEQ_1:def 7;
hence ((p ^ q) ^ r) . k = q . (k - (len p)) by A7, FINSEQ_1:32; :: thesis: verum