let a be Element of NAT ; :: thesis: for fs, fs1, fs2 being FinSequence
for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds
Del (fs,a) = fs1 ^ fs2

let fs, fs1, fs2 be FinSequence; :: thesis: for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds
Del (fs,a) = fs1 ^ fs2

let v be set ; :: thesis: ( a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 implies Del (fs,a) = fs1 ^ fs2 )
assume that
A1: a in dom fs and
A2: fs = (fs1 ^ <*v*>) ^ fs2 and
A3: len fs1 = a - 1 ; :: thesis: Del (fs,a) = fs1 ^ fs2
A4: (len (Del (fs,a))) + 1 = len fs by ;
len fs = (len (fs1 ^ <*v*>)) + (len fs2) by
.= ((len fs1) + 1) + (len fs2) by FINSEQ_2:16
.= a + (len fs2) by A3 ;
then len (Del (fs,a)) = (len fs2) + (len fs1) by A3, A4;
then A5: len (fs1 ^ fs2) = len (Del (fs,a)) by FINSEQ_1:22;
A6: len <*v*> = 1 by FINSEQ_1:39;
A7: fs = fs1 ^ (<*v*> ^ fs2) by ;
then len fs = (a - 1) + (len (<*v*> ^ fs2)) by ;
then A8: len (<*v*> ^ fs2) = (len fs) - (a - 1) ;
now :: thesis: for e being Nat st 1 <= e & e <= len (Del (fs,a)) holds
(fs1 ^ fs2) . e = (Del (fs,a)) . e
let e be Nat; :: thesis: ( 1 <= e & e <= len (Del (fs,a)) implies (fs1 ^ fs2) . e = (Del (fs,a)) . e )
assume that
A9: 1 <= e and
A10: e <= len (Del (fs,a)) ; :: thesis: (fs1 ^ fs2) . e = (Del (fs,a)) . e
reconsider e1 = e as Element of NAT by ORDINAL1:def 12;
now :: thesis: (fs1 ^ fs2) . e = (Del (fs,a)) . e
per cases ( e < a or e >= a ) ;
suppose A11: e < a ; :: thesis: (fs1 ^ fs2) . e = (Del (fs,a)) . e
then e1 <= a - 1 by Lm39;
then A12: e in dom fs1 by ;
hence (fs1 ^ fs2) . e = fs1 . e by FINSEQ_1:def 7
.= fs . e1 by
.= (Del (fs,a)) . e by ;
:: thesis: verum
end;
suppose A13: e >= a ; :: thesis: (fs1 ^ fs2) . e = (Del (fs,a)) . e
then A14: e1 > a - 1 by Lm39;
then A15: e + 1 > a by XREAL_1:19;
then (e + 1) - a > 0 by XREAL_1:50;
then A16: ((e + 1) - a) + 1 > 0 + 1 by XREAL_1:6;
A17: e + 1 > a - 1 by ;
then (e + 1) - (a - 1) > 0 by XREAL_1:50;
then reconsider f = (e + 1) - (a - 1) as Element of NAT by INT_1:3;
A18: e + 1 <= len fs by ;
then A19: (e + 1) - (a - 1) <= len (<*v*> ^ fs2) by ;
thus (fs1 ^ fs2) . e = fs2 . (e - (len fs1)) by
.= fs2 . (f - 1) by A3
.= (<*v*> ^ fs2) . f by
.= (fs1 ^ (<*v*> ^ fs2)) . (e1 + 1) by
.= (Del (fs,a)) . e by ; :: thesis: verum
end;
end;
end;
hence (fs1 ^ fs2) . e = (Del (fs,a)) . e ; :: thesis: verum
end;
hence Del (fs,a) = fs1 ^ fs2 by A5; :: thesis: verum