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 A1: ( len f = n + 1 & x = f . (n + 1) ) ; :: thesis: f = (f | n) ^ <*x*>
set fn = f | n;
A2: n <= n + 1 by NAT_1:11;
A3: len (f | n) = n by A1, FINSEQ_1:80, NAT_1:11;
then A4: len ((f | n) ^ <*x*>) = n + (len <*x*>) by FINSEQ_1:35
.= len f by A1, FINSEQ_1:57 ;
X: dom f = Seg (len f) by FINSEQ_1:def 3;

now

let m be Nat; :: thesis: ( m in dom f implies f . m = ((f | n) ^ <*x*>) . m )
assume m in dom f ; :: thesis: f . m = ((f | n) ^ <*x*>) . m
then A5: ( 1 <= m & m <= len f ) by X, FINSEQ_1:3;

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, A3, FINSEQ_1:59; :: thesis: verum

end;

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

then m < n + 1 by A1, A5, XXREAL_0:1;
then A6: m <= n by NAT_1:13;
then A7: m in dom (f | n) by A3, A5, FINSEQ_3:27;
1 <= n by A5, A6, XXREAL_0:2;
then A8: n in dom f by A1, A2, FINSEQ_3:27;
A9: Seg (len (f | n)) = dom (f | n) by FINSEQ_1:def 3;
thus ((f | n) ^ <*x*>) . m = (f | n) . m by A7, FINSEQ_1:def 7
.= f . m by A3, A7, A8, A9, Th19 ; :: thesis: verum

end;

end;

end;

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

end;

hence f = (f | n) ^ <*x*> by A4, FINSEQ_2:10; :: thesis: verum