let D be non empty set ; :: thesis: for k, n being Nat
for f being FinSequence of D * st k in dom (f . (n + 1)) holds
(f . (n + 1)) . k = ((D -concatenation) "**" f) . (k + (len ((D -concatenation) "**" (f | n))))
let k, n be Nat; :: thesis: for f being FinSequence of D * st k in dom (f . (n + 1)) holds
(f . (n + 1)) . k = ((D -concatenation) "**" f) . (k + (len ((D -concatenation) "**" (f | n))))
let f be FinSequence of D * ; :: thesis: ( k in dom (f . (n + 1)) implies (f . (n + 1)) . k = ((D -concatenation) "**" f) . (k + (len ((D -concatenation) "**" (f | n)))) )
set DC = D -concatenation ;
set n1 = n + 1;
assume A1: k in dom (f . (n + 1)) ; :: thesis: (f . (n + 1)) . k = ((D -concatenation) "**" f) . (k + (len ((D -concatenation) "**" (f | n))))
then f . (n + 1) <> {} ;
then A2: n + 1 in dom f by FUNCT_1:def 2;
then n + 1 <= len f by FINSEQ_3:25;
then A3: f | (n + 1) = (f | n) ^ <*(f /. (n + 1))*> by FINSEQ_5:82;
A4: f . (n + 1) = f /. (n + 1) by A2, PARTFUN1:def 6;
consider q being FinSequence such that
A5: f = (f | (n + 1)) ^ q by FINSEQ_1:80;
reconsider q = q as FinSequence of D * by A5, FINSEQ_1:36;
A6: (D -concatenation) "**" (f | (n + 1)) = ((D -concatenation) "**" (f | n)) ^ ((D -concatenation) "**" <*(f /. (n + 1))*>) by A3, Th3
.= ((D -concatenation) "**" (f | n)) ^ (f /. (n + 1)) by FINSOP_1:11 ;
then A7: ((D -concatenation) "**" (f | (n + 1))) . (k + (len ((D -concatenation) "**" (f | n)))) = (f . (n + 1)) . k by A4, A1, FINSEQ_1:def 7;
A8: k + (len ((D -concatenation) "**" (f | n))) in dom ((D -concatenation) "**" (f | (n + 1))) by A6, A4, A1, FINSEQ_1:28;
(D -concatenation) "**" f = ((D -concatenation) "**" (f | (n + 1))) ^ ((D -concatenation) "**" q) by A5, Th3;
hence (f . (n + 1)) . k = ((D -concatenation) "**" f) . (k + (len ((D -concatenation) "**" (f | n)))) by A8, FINSEQ_1:def 7, A7; :: thesis: verum