let n be Nat; :: thesis: for m being non zero Nat
for f being n + b₁ -element FinSequence holds f | (n + 1) = (f | n) ^ <*(f . (n + 1))*>
let m be non zero Nat; :: thesis: for f being n + m -element FinSequence holds f | (n + 1) = (f | n) ^ <*(f . (n + 1))*>
let f be n + m -element FinSequence; :: thesis: f | (n + 1) = (f | n) ^ <*(f . (n + 1))*>
A0: n + 1 > n + 0 by XREAL_1:6;
n + m >= n + 1 by XREAL_1:6, NAT_1:14;
then len f >= n + 1 by CARD_1:def 7;
then A1: len (f | (n + 1)) = n + 1 by FINSEQ_1:59;
n + 1 >= 0 + 1 by XREAL_1:6;
then A2: ((f | (n + 1)) ^ (f /^ (n + 1))) . (n + 1) = (f | (n + 1)) . (n + 1) by A1, FINSEQ_1:64;
f | (n + 1) is n + 1 -element FinSequence by A1, CARD_1:def 7;
then f | (n + 1) = ((f | (n + 1)) | n) ^ <*((f | (n + 1)) . (n + 1))*> by LmFNK
.= (f | n) ^ <*(f . (n + 1))*> by A0, A2, FINSEQ_1:82 ;
hence f | (n + 1) = (f | n) ^ <*(f . (n + 1))*> ; :: thesis: verum