let D be set ; :: thesis: for Y being FinSequenceSet of D
for F being FinSequence of Y
for k being Nat st k < len F holds
Length (F | (k + 1)) = (Length (F | k)) ^ <*(len (F . (k + 1)))*>
let Y be FinSequenceSet of D; :: thesis: for F being FinSequence of Y
for k being Nat st k < len F holds
Length (F | (k + 1)) = (Length (F | k)) ^ <*(len (F . (k + 1)))*>
let F be FinSequence of Y; :: thesis: for k being Nat st k < len F holds
Length (F | (k + 1)) = (Length (F | k)) ^ <*(len (F . (k + 1)))*>
let k be Nat; :: thesis: ( k < len F implies Length (F | (k + 1)) = (Length (F | k)) ^ <*(len (F . (k + 1)))*> )
assume A1: k < len F ; :: thesis: Length (F | (k + 1)) = (Length (F | k)) ^ <*(len (F . (k + 1)))*>
then k + 1 <= len F by NAT_1:13;
then A3: len (F | (k + 1)) = k + 1 by FINSEQ_1:59;
A6: len (F | k) = k by A1, FINSEQ_1:59;
A5: ( dom (Length (F | (k + 1))) = dom (F | (k + 1)) & dom (Length (F | k)) = dom (F | k) ) by Def1;
then A7: ( len (Length (F | (k + 1))) = k + 1 & len (Length (F | k)) = k ) by A3, A6, FINSEQ_3:29;
then A8: len ((Length (F | k)) ^ <*(len (F . (k + 1)))*>) = k + (len <*(len (F . (k + 1)))*>) by FINSEQ_1:22
.= k + 1 by FINSEQ_1:40 ;

now :: thesis: for n being Nat st 1 <= n & n <= len (Length (F | (k + 1))) holds
(Length (F | (k + 1))) . n = ((Length (F | k)) ^ <*(len (F . (k + 1)))*>) . n

let n be Nat; :: thesis: ( 1 <= n & n <= len (Length (F | (k + 1))) implies (Length (F | (k + 1))) . b₁ = ((Length (F | k)) ^ <*(len (F . (k + 1)))*>) . b₁ )
assume A9: ( 1 <= n & n <= len (Length (F | (k + 1))) ) ; :: thesis: (Length (F | (k + 1))) . b₁ = ((Length (F | k)) ^ <*(len (F . (k + 1)))*>) . b₁
then n in dom (Length (F | (k + 1))) by FINSEQ_3:25;
then A10: (Length (F | (k + 1))) . n = len ((F | (k + 1)) . n) by Def1
.= len (F . n) by A7, A9, FINSEQ_3:112 ;

per cases ( n = len (Length (F | (k + 1))) or n <> len (Length (F | (k + 1))) ) ;

suppose n = len (Length (F | (k + 1))) ; :: thesis: (Length (F | (k + 1))) . b₁ = ((Length (F | k)) ^ <*(len (F . (k + 1)))*>) . b₁

hence (Length (F | (k + 1))) . n = ((Length (F | k)) ^ <*(len (F . (k + 1)))*>) . n by A7, A10, FINSEQ_1:42; :: thesis: verum

end;

suppose n <> len (Length (F | (k + 1))) ; :: thesis: (Length (F | (k + 1))) . b₁ = ((Length (F | k)) ^ <*(len (F . (k + 1)))*>) . b₁

then n < k + 1 by A7, A9, XXREAL_0:1;
then A11: n <= k by NAT_1:13;
then ((Length (F | k)) ^ <*(len (F . (k + 1)))*>) . n = (Length (F | k)) . n by A9, A7, FINSEQ_1:64
.= len ((F | k) . n) by A11, Def1, A9, A5, A6, FINSEQ_3:25
.= len (F . n) by A11, FINSEQ_3:112 ;
hence (Length (F | (k + 1))) . n = ((Length (F | k)) ^ <*(len (F . (k + 1)))*>) . n by A10; :: thesis: verum

end;

end;

end;

hence Length (F | (k + 1)) = (Length (F | k)) ^ <*(len (F . (k + 1)))*> by A5, A8, A3, FINSEQ_3:29; :: thesis: verum