let D be non empty set ; :: thesis: for f being FinSequence of D
for n being Nat
for x being set st len f = n + 1 & x = f . (n + 1) holds
f = (f | n) ^ <*x*>
let f be FinSequence of D; :: thesis: for n being Nat
for x being set st len f = n + 1 & x = f . (n + 1) holds
f = (f | n) ^ <*x*>
let n be Nat; :: thesis: for x being set st len f = n + 1 & x = f . (n + 1) holds
f = (f | n) ^ <*x*>
let x be set ; :: thesis: ( len f = n + 1 & x = f . (n + 1) implies f = (f | n) ^ <*x*> )
assume that
A1: len f = n + 1 and
A2: x = f . (n + 1) ; :: thesis: f = (f | n) ^ <*x*>
set fn = f | n;
A3: len (f | n) = n by A1, FINSEQ_1:59, NAT_1:11;
A4: dom f = Seg (len f) by FINSEQ_1:def 3;
A5: n <= n + 1 by NAT_1:11;

A6: now

let m be Nat; :: thesis: ( m in dom f implies f . m = ((f | n) ^ <*x*>) . m )
assume A7: m in dom f ; :: thesis: f . m = ((f | n) ^ <*x*>) . m
then A8: 1 <= m by A4, FINSEQ_1:1;
A9: m <= len f by A4, A7, FINSEQ_1:1;

now

per cases ( m = len f or m <> len f ) ;

case m = len f ; :: thesis: f . m = ((f | n) ^ <*x*>) . m

hence f . m = ((f | n) ^ <*x*>) . m by A1, A2, A3, FINSEQ_1:42; :: thesis: verum

end;

case m <> len f ; :: thesis: ((f | n) ^ <*x*>) . m = f . m

then m < n + 1 by A1, A9, XXREAL_0:1;
then A10: m <= n by NAT_1:13;
then 1 <= n by A8, XXREAL_0:2;
then A11: n in dom f by A1, A5, FINSEQ_3:25;
A12: Seg (len (f | n)) = dom (f | n) by FINSEQ_1:def 3;
A13: m in dom (f | n) by A3, A8, A10, FINSEQ_3:25;
hence ((f | n) ^ <*x*>) . m = (f | n) . m by FINSEQ_1:def 7
.= f . m by A3, A13, A11, A12, Th19 ;
:: thesis: verum

end;

end;

end;

hence f . m = ((f | n) ^ <*x*>) . m ; :: thesis: verum

end;

len ((f | n) ^ <*x*>) = n + (len <*x*>) by A3, FINSEQ_1:22
.= len f by A1, FINSEQ_1:40 ;
hence f = (f | n) ^ <*x*> by A6, FINSEQ_2:9; :: thesis: verum