let a be Nat; :: thesis: for fs, fs1, fs2 being FinSequence
for v being object 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 object st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds
Del (fs,a) = fs1 ^ fs2
let v be object ; :: 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 A1, Def1;
len fs = (len (fs1 ^ <*v*>)) + (len fs2) by A2, FINSEQ_1:22
.= ((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 A2, FINSEQ_1:32;
then len fs = (a - 1) + (len (<*v*> ^ fs2)) by A3, FINSEQ_1:22;
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

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 e <= a - 1 by Lm8;
then A12: e in dom fs1 by A3, A9, FINSEQ_3:25;
hence (fs1 ^ fs2) . e = fs1 . e by FINSEQ_1:def 7
.= fs . e by A7, A12, FINSEQ_1:def 7
.= (Del (fs,a)) . e by A1, A11, Def1 ;
:: thesis: verum

end;

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

then A14: e > a - 1 by Lm8;
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 A15, XREAL_1:146, XXREAL_0:2;
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 A4, A10, XREAL_1:6;
then A19: (e + 1) - (a - 1) <= len (<*v*> ^ fs2) by A8, XREAL_1:9;
thus (fs1 ^ fs2) . e = fs2 . (e - (len fs1)) by A3, A5, A10, A14, FINSEQ_1:24
.= fs2 . (f - 1) by A3
.= (<*v*> ^ fs2) . f by A6, A16, A19, FINSEQ_1:24
.= (fs1 ^ (<*v*> ^ fs2)) . (e + 1) by A3, A7, A17, A18, FINSEQ_1:24
.= (Del (fs,a)) . e by A1, A7, A13, Def1 ; :: 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