let D be non empty set ; :: thesis: for F being XFinSequence of
for n being Element of NAT st len F = n + 1 holds
F = (F | n) ^ <%(F . n)%>
let F be XFinSequence of ; :: 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 & len <%x%> = 1 & ((len f) + 1) - 1 = len f & (n + 1) - 1 = n ) by A1, A2, AFINSQ_1:20, AFINSQ_1:38;
then ( len f = n & n <= len F ) by A1, NAT_1:13;
then A4: ( len f = n & 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 A5: x in dom f ; :: thesis: f . x = (F | n) . x
reconsider k = x as Element of NAT by A5;
( F . k = (F | n) . k & f . k = F . k ) by A2, A4, A5, AFINSQ_1:def 4, FUNCT_1:70;
hence f . x = (F | n) . x ; :: thesis: verum

end;

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