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: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

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: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

hence
Del ((fp ^ <*d*>),b) = (Del (fp,b)) ^ <*d*>
by A4, A5, FINSEQ_3:109; :: thesis: verum
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:25;

end;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:25;

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

end;

suppose A10:
k < b
; :: thesis: (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; :: thesis: verum

end;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; :: thesis: verum

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

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

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

end;

suppose A14:
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: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; :: thesis: verum

end;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; :: thesis: verum