let D be non empty set ; :: thesis: for F being XFinSequence of D
for n being Element of NAT st len F = n + 1 holds
F = (F | n) ^ <%(F . n)%>
let F be XFinSequence of D; :: thesis: for n being Element of NAT st len F = n + 1 holds
F = (F | n) ^ <%(F . n)%>
let n be Element of NAT ; :: thesis: ( len F = n + 1 implies F = (F | n) ^ <%(F . n)%> )
assume A1: len F = n + 1 ; :: thesis: F = (F | n) ^ <%(F . n)%>
consider f being XFinSequence, x being set such that
A2: F = f ^ <%x%> by A1, AFINSQ_1:44, CARD_1:47;
A3: (len f) + (len <%x%>) = n + 1 by A1, A2, AFINSQ_1:20;
A4: len <%x%> = 1 by AFINSQ_1:38;
n <= len F by A1, NAT_1:13;
then A5: len (F | n) = n by Lm2;
for x being set st x in dom f holds
f . x = (F | n) . x

proof

let x be set ; :: thesis: ( x in dom f implies f . x = (F | n) . x )
assume A6: x in dom f ; :: thesis: f . x = (F | n) . x
reconsider k = x as Element of NAT by A6;
F . k = (F | n) . k by A3, A4, A5, A6, FUNCT_1:70;
hence f . x = (F | n) . x by A2, A6, AFINSQ_1:def 4; :: thesis: verum

end;

then f = F | n by A3, A4, A5, FUNCT_1:9;
hence F = (F | n) ^ <%(F . n)%> by A2, A3, A4, AFINSQ_1:40; :: thesis: verum