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 A1, WSIERP_1:def 1;

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) ;

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 A1, WSIERP_1:def 1;

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

hence
Del (fs,a) = fs1 ^ fs2
by A5; :: thesis: verum(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

end;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)) . eend;

hence
(fs1 ^ fs2) . e = (Del (fs,a)) . e
; :: thesis: verumper cases
( e < a or e >= a )
;

end;

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

then
e <= a - 1
by Lm4;

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, WSIERP_1:def 1 ;

:: thesis: verum

end;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, WSIERP_1:def 1 ;

:: thesis: verum

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

then A14:
e > a - 1
by Lm4;

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, WSIERP_1:def 1 ; :: thesis: verum

end;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, WSIERP_1:def 1 ; :: thesis: verum