let fp be FinSequence of NAT ; 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 ; ( 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
; Del ((fp ^ <*d*>),b) = (Del (fp,b)) ^ <*d*>
A3:
len (Del (fp,b)) = n
by A1, A2, FINSEQ_3:109;
then A4:
len ((Del (fp,b)) ^ <*d*>) = n + 1
by FINSEQ_2:16;
A5:
( len (fp ^ <*d*>) = (n + 1) + 1 & b in dom (fp ^ <*d*>) )
by A1, A2, FINSEQ_2:16, FINSEQ_3:22;
then A6:
len (Del ((fp ^ <*d*>),b)) = len ((Del (fp,b)) ^ <*d*>)
by A4, FINSEQ_3:109;
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;
( 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))
;
(Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k
A9:
k in dom fp
by A2, A4, A6, A7, A8, FINSEQ_3:25;
per cases
( k < b or b <= k )
;
suppose A10:
k < b
;
(Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k
b <= n + 1
by A1, A2, FINSEQ_3:25;
then
k < n + 1
by A10, XXREAL_0:2;
then
k <= n
by NAT_1:13;
then
k in dom (Del (fp,b))
by A3, A7, FINSEQ_3:25;
then A11:
((Del (fp,b)) ^ <*d*>) . k =
(Del (fp,b)) . k
by FINSEQ_1:def 7
.=
fp . k
by A10, FINSEQ_3:110
;
set fpd =
fp ^ <*d*>;
(Del ((fp ^ <*d*>),b)) . k =
(fp ^ <*d*>) . k
by A10, FINSEQ_3:110
.=
fp . k
by A9, FINSEQ_1:def 7
;
hence
(Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k
by A11;
verum end; suppose A12:
b <= k
;
(Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . kthen A13:
(Del ((fp ^ <*d*>),b)) . k = (fp ^ <*d*>) . (k + 1)
by A4, A5, A6, A8, FINSEQ_3:111;
per cases
( k <= n or k = n + 1 )
by A4, A6, A8, NAT_1:8;
suppose A14:
k <= n
;
(Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . kthen
k in dom (Del (fp,b))
by A3, A7, FINSEQ_3:25;
then A15:
((Del (fp,b)) ^ <*d*>) . k =
(Del (fp,b)) . k
by FINSEQ_1:def 7
.=
fp . (k + 1)
by A1, A2, A12, A14, FINSEQ_3:111
;
A16:
k + 1
>= 1
by NAT_1:11;
k + 1
<= n + 1
by A14, XREAL_1:6;
then
k + 1
in dom fp
by A2, A16, FINSEQ_3:25;
hence
(Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k
by A13, A15, FINSEQ_1:def 7;
verum end; end; end; end;
end;
hence
Del ((fp ^ <*d*>),b) = (Del (fp,b)) ^ <*d*>
by A4, A5, FINSEQ_3:109; verum