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 A1: ( a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 ) ; :: thesis: Del fs,a = fs1 ^ fs2
then A2: len fs = (len (fs1 ^ <*v*>)) + (len fs2) by FINSEQ_1:35
.= ((len fs1) + 1) + (len fs2) by FINSEQ_2:19
.= a + (len fs2) by A1 ;
A3: fs = fs1 ^ (<*v*> ^ fs2) by A1, FINSEQ_1:45;
A4: len <*v*> = 1 by FINSEQ_1:56;
len fs = (a - 1) + (len (<*v*> ^ fs2)) by A1, A3, FINSEQ_1:35;
then A5: len (<*v*> ^ fs2) = (len fs) - (a - 1) ;
A6: (len (Del fs,a)) + 1 = len fs by A1, WSIERP_1:def 1;
then len (Del fs,a) = (len fs2) + (len fs1) by A1, A2;
then A7: len (fs1 ^ fs2) = len (Del fs,a) by FINSEQ_1:35;

now

let e be Nat; :: thesis: ( 1 <= e & e <= len (Del fs,a) implies (fs1 ^ fs2) . e = (Del fs,a) . e )
assume A8: ( 1 <= e & e <= len (Del fs,a) ) ; :: thesis: (fs1 ^ fs2) . e = (Del fs,a) . e

now

per cases ( e < a or e >= a ) ;

suppose A9: e < a ; :: thesis: (fs1 ^ fs2) . e = (Del fs,a) . e

then e <= a - 1 by Lm4;
then A10: e in dom fs1 by A1, A8, FINSEQ_3:27;
hence (fs1 ^ fs2) . e = fs1 . e by FINSEQ_1:def 7
.= fs . e by A3, A10, FINSEQ_1:def 7
.= (Del fs,a) . e by A1, A9, WSIERP_1:def 1 ;
:: thesis: verum

end;

suppose A11: e >= a ; :: thesis: (fs1 ^ fs2) . e = (Del fs,a) . e

then A12: e > a - 1 by Lm4;
then A13: e + 1 > a by XREAL_1:21;
then (e + 1) - a > 0 by XREAL_1:52;
then A14: ((e + 1) - a) + 1 > 0 + 1 by XREAL_1:8;
A15: e + 1 > a - 1 by A13, XREAL_1:148, XXREAL_0:2;
then (e + 1) - (a - 1) > 0 by XREAL_1:52;
then reconsider f = (e + 1) - (a - 1) as Element of NAT by INT_1:16;
A16: e + 1 <= len fs by A6, A8, XREAL_1:8;
then A17: (e + 1) - (a - 1) <= len (<*v*> ^ fs2) by A5, XREAL_1:11;
thus (fs1 ^ fs2) . e = fs2 . (e - (len fs1)) by A1, A7, A8, A12, FINSEQ_1:37
.= fs2 . (f - 1) by A1
.= (<*v*> ^ fs2) . f by A4, A14, A17, FINSEQ_1:37
.= (fs1 ^ (<*v*> ^ fs2)) . (e + 1) by A1, A3, A15, A16, FINSEQ_1:37
.= (Del fs,a) . e by A1, A3, A11, WSIERP_1:def 1 ; :: thesis: verum

end;

end;

end;

hence (fs1 ^ fs2) . e = (Del fs,a) . e ; :: thesis: verum

end;

hence Del fs,a = fs1 ^ fs2 by A7, FINSEQ_1:18; :: thesis: verum