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:19;
A3: h . (n + 1) = f . (n + 1) by FINSEQ_1:6, FUNCT_1:72;
n <= n + 1 by NAT_1:11;
then Seg n c= Seg (n + 1) by FINSEQ_1:7;
then A4: g = h | (Seg n) by A2, FUNCT_1:82;
n + 1 <= len f by A1, FINSEQ_3:27;
then len h = n + 1 by FINSEQ_1:21;
hence f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*> by A3, A4, FINSEQ_3:61; :: thesis: verum