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 ;
A4: dom f = Seg (len f) by FINSEQ_1:def 3;
A5: n <= n + 1 by NAT_1:11;
A6: now :: thesis: for m being Nat st m in dom f holds
f . m = ((f | n) ^ <*x*>) . m
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 ;
A9: m <= len f by ;
now :: thesis: ( ( m = len f & f . m = ((f | n) ^ <*x*>) . m ) or ( m <> len f & ((f | n) ^ <*x*>) . m = f . m ) )
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 ; :: thesis: verum
end;
case m <> len f ; :: thesis: ((f | n) ^ <*x*>) . m = f . m
then m < n + 1 by ;
then A10: m <= n by NAT_1:13;
then 1 <= n by ;
then A11: n in dom f by ;
A12: Seg (len (f | n)) = dom (f | n) by FINSEQ_1:def 3;
A13: m in dom (f | n) by ;
hence ((f | n) ^ <*x*>) . m = (f | n) . m by FINSEQ_1:def 7
.= f . m by A3, A13, A11, A12, Th6 ;
:: thesis: verum
end;
end;
end;
hence f . m = ((f | n) ^ <*x*>) . m ; :: thesis: verum
end;
len ((f | n) ^ <*x*>) = n + () by
.= len f by ;
hence f = (f | n) ^ <*x*> by ; :: thesis: verum