let n be Nat; :: thesis: for f, g being FinSequence st n + 1 in dom f & g = f | (Seg n) holds
f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*>
let f, g be FinSequence; :: thesis: ( n + 1 in dom f & g = f | (Seg n) implies f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*> )
assume that
A1: n + 1 in dom f and
A2: g = f | (Seg n) ; :: thesis: f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*>
reconsider h = f | (Seg (n + 1)) as FinSequence by FINSEQ_1:15;
n + 1 <= len f by A1, FINSEQ_3:25;
then A3: len h = n + 1 by FINSEQ_1:17;
Seg n c= Seg (n + 1) by FINSEQ_1:5, NAT_1:11;
then ( h . (n + 1) = f . (n + 1) & g = h | (Seg n) ) by A2, FINSEQ_1:4, FUNCT_1:49, FUNCT_1:51;
hence f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*> by A3, FINSEQ_3:55; :: thesis: verum