let fp be FinSequence of NAT ; :: thesis: for d, b, n being Element of NAT st b in dom fp & len fp = n + 1 holds
Del (fp ^ <*d*>),b = (Del fp,b) ^ <*d*>
let d, b, n be Element of NAT ; :: thesis: ( b in dom fp & len fp = n + 1 implies Del (fp ^ <*d*>),b = (Del fp,b) ^ <*d*> )
assume that
A1: b in dom fp and
A2: len fp = n + 1 ; :: thesis: Del (fp ^ <*d*>),b = (Del fp,b) ^ <*d*>
A3: len (Del fp,b) = n by A1, A2, FINSEQ_3:118;
then A4: len ((Del fp,b) ^ <*d*>) = n + 1 by FINSEQ_2:19;
A5: ( len (fp ^ <*d*>) = (n + 1) + 1 & b in dom (fp ^ <*d*>) ) by A1, A2, FINSEQ_2:19, FINSEQ_3:24;
then A6: len (Del (fp ^ <*d*>),b) = len ((Del fp,b) ^ <*d*>) by A4, FINSEQ_3:118;
for k being Nat st 1 <= k & k <= len (Del (fp ^ <*d*>),b) holds
(Del (fp ^ <*d*>),b) . k = ((Del fp,b) ^ <*d*>) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (Del (fp ^ <*d*>),b) implies (Del (fp ^ <*d*>),b) . k = ((Del fp,b) ^ <*d*>) . k )
assume that
A7: 1 <= k and
A8: k <= len (Del (fp ^ <*d*>),b) ; :: thesis: (Del (fp ^ <*d*>),b) . k = ((Del fp,b) ^ <*d*>) . k
A9: k in dom fp by A2, A4, A6, A7, A8, FINSEQ_3:27;

per cases ( k < b or b <= k ) ;

suppose A11: k < b ; :: thesis: (Del (fp ^ <*d*>),b) . k = ((Del fp,b) ^ <*d*>) . k

b <= n + 1 by A1, A2, FINSEQ_3:27;
then k < n + 1 by A11, XXREAL_0:2;
then k <= n by NAT_1:13;
then k in dom (Del fp,b) by A3, A7, FINSEQ_3:27;
then A12: ((Del fp,b) ^ <*d*>) . k = (Del fp,b) . k by FINSEQ_1:def 7
.= fp . k by A11, FINSEQ_3:119 ;
set fpd = fp ^ <*d*>;
reconsider w = n + 1 as Element of NAT by ORDINAL1:def 13;
(Del (fp ^ <*d*>),b) . k = (fp ^ <*d*>) . k by A11, FINSEQ_3:119
.= fp . k by A9, FINSEQ_1:def 7 ;
hence (Del (fp ^ <*d*>),b) . k = ((Del fp,b) ^ <*d*>) . k by A12; :: thesis: verum

end;

suppose A13: b <= k ; :: thesis: (Del (fp ^ <*d*>),b) . k = ((Del fp,b) ^ <*d*>) . k

then A14: (Del (fp ^ <*d*>),b) . k = (fp ^ <*d*>) . (k + 1) by A4, A5, A6, A8, FINSEQ_3:120;

per cases ( k <= n or k = n + 1 ) by A4, A6, A8, NAT_1:8;

suppose A15: k <= n ; :: thesis: (Del (fp ^ <*d*>),b) . k = ((Del fp,b) ^ <*d*>) . k

then k in dom (Del fp,b) by A3, A7, FINSEQ_3:27;
then A16: ((Del fp,b) ^ <*d*>) . k = (Del fp,b) . k by FINSEQ_1:def 7
.= fp . (k + 1) by A1, A2, A13, A15, FINSEQ_3:120 ;
A17: k + 1 >= 1 by NAT_1:11;
k + 1 <= n + 1 by A15, XREAL_1:8;
then k + 1 in dom fp by A2, A17, FINSEQ_3:27;
hence (Del (fp ^ <*d*>),b) . k = ((Del fp,b) ^ <*d*>) . k by A14, A16, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A18: k = n + 1 ; :: thesis: (Del (fp ^ <*d*>),b) . k = ((Del fp,b) ^ <*d*>) . k

then (Del (fp ^ <*d*>),b) . k = d by A2, A14, FINSEQ_1:59;
hence (Del (fp ^ <*d*>),b) . k = ((Del fp,b) ^ <*d*>) . k by A3, A18, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

end;

end;

hence Del (fp ^ <*d*>),b = (Del fp,b) ^ <*d*> by A4, A5, FINSEQ_1:18, FINSEQ_3:118; :: thesis: verum