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:11;
0 + 1 = 1 ;
then A4: 1 <= k - (len p) by A3, INT_1:20;
then reconsider n = k - (len p) as Nat by Th3;
A5: ((len p) + (len q)) - (len p) = len q ;
k <= (len p) + (len q) by A2, FINSEQ_1:35;
then n <= len q by A5, XREAL_1:11;
then n in Seg (len q) by A4, FINSEQ_1:3;
then A6: n in dom q by FINSEQ_1:def 3;
len (p ^ q) <= len (p ^ (q ^ r)) by Th11;
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:37;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
(q ^ r) . n = q . n by A6, FINSEQ_1:def 7;
hence ((p ^ q) ^ r) . k = q . (k - (len p)) by A7, FINSEQ_1:45; :: thesis: verum