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
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:25;
per cases ( k < b or b <= k ) ;
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;
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;
per cases ( k <= n or k = n + 1 ) by A4, A6, A8, NAT_1:8;
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;
suppose A17: k = n + 1 ; :: thesis: (Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k
then (Del ((fp ^ <*d*>),b)) . k = d by A2, A13, FINSEQ_1:42;
hence (Del ((fp ^ <*d*>),b)) . k = ((Del (fp,b)) ^ <*d*>) . k by A3, A17, FINSEQ_1:42; :: thesis: verum
end;
end;
end;
end;
end;
hence Del ((fp ^ <*d*>),b) = (Del (fp,b)) ^ <*d*> by A4, A5, FINSEQ_3:109; :: thesis: verum