let a be Element of NAT ; :: thesis: for fs1, fs2 being FinSequence holds
( ( a <= len fs1 implies Del (fs1 ^ fs2),a = (Del fs1,a) ^ fs2 ) & ( a >= 1 implies Del (fs1 ^ fs2),((len fs1) + a) = fs1 ^ (Del fs2,a) ) )
let fs1, fs2 be FinSequence; :: thesis: ( ( a <= len fs1 implies Del (fs1 ^ fs2),a = (Del fs1,a) ^ fs2 ) & ( a >= 1 implies Del (fs1 ^ fs2),((len fs1) + a) = fs1 ^ (Del fs2,a) ) )
set f = fs1 ^ fs2;
A1: ( len (fs1 ^ fs2) = (len fs1) + (len fs2) & len ((Del fs1,a) ^ fs2) = (len (Del fs1,a)) + (len fs2) & len (fs1 ^ (Del fs2,a)) = (len fs1) + (len (Del fs2,a)) ) by FINSEQ_1:35;

A2: now

assume A3: a <= len fs1 ; :: thesis: Del (fs1 ^ fs2),a = (Del fs1,a) ^ fs2
set f1 = Del (fs1 ^ fs2),a;
set f2 = (Del fs1,a) ^ fs2;
set f3 = <*((fs1 ^ fs2) . a)*>;
len fs1 <= len (fs1 ^ fs2) by A1, NAT_1:11;
then A4: a <= len (fs1 ^ fs2) by A3, XXREAL_0:2;

now

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

suppose a < 1 ; :: thesis: Del (fs1 ^ fs2),a = (Del fs1,a) ^ fs2

then A5: ( not a in dom fs1 & not a in dom (fs1 ^ fs2) ) by FINSEQ_3:27;
hence Del (fs1 ^ fs2),a = fs1 ^ fs2 by WSIERP_1:def 1
.= (Del fs1,a) ^ fs2 by A5, WSIERP_1:def 1 ;
:: thesis: verum

end;

suppose a >= 1 ; :: thesis: Del (fs1 ^ fs2),a = (Del fs1,a) ^ fs2

then A6: ( a in dom (fs1 ^ fs2) & a in dom fs1 ) by A3, A4, FINSEQ_3:27;
then consider g1, g2 being FinSequence such that
A7: ( fs1 ^ fs2 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ g2 & len g1 = a - 1 & len g2 = (len (fs1 ^ fs2)) - a ) by Lm41;
len (g1 ^ <*((fs1 ^ fs2) . a)*>) = (a - 1) + 1 by A7, FINSEQ_2:19
.= a ;
then consider t being FinSequence such that
A8: fs1 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ t by A3, A7, FINSEQ_1:64;
A9: Del fs1,a = g1 ^ t by A6, A7, A8, Lm42;
(g1 ^ <*((fs1 ^ fs2) . a)*>) ^ g2 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ (t ^ fs2) by A7, A8, FINSEQ_1:45;
then A10: g2 = t ^ fs2 by FINSEQ_1:46;
thus Del (fs1 ^ fs2),a = g1 ^ g2 by A6, A7, Lm42
.= (Del fs1,a) ^ fs2 by A9, A10, FINSEQ_1:45 ; :: thesis: verum

end;

end;

end;

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

end;

now

assume A11: a >= 1 ; :: thesis: Del (fs1 ^ fs2),((len fs1) + a) = fs1 ^ (Del fs2,a)
set f1 = Del (fs1 ^ fs2),((len fs1) + a);
set f2 = fs1 ^ (Del fs2,a);

now

per cases ( a > len fs2 or a <= len fs2 ) ;

suppose A12: a > len fs2 ; :: thesis: Del (fs1 ^ fs2),((len fs1) + a) = fs1 ^ (Del fs2,a)

then A13: not a in dom fs2 by FINSEQ_3:27;
(len fs1) + a > len (fs1 ^ fs2) by A1, A12, XREAL_1:8;
then not (len fs1) + a in dom (fs1 ^ fs2) by FINSEQ_3:27;
hence Del (fs1 ^ fs2),((len fs1) + a) = fs1 ^ fs2 by WSIERP_1:def 1
.= fs1 ^ (Del fs2,a) by A13, WSIERP_1:def 1 ;
:: thesis: verum

end;

suppose A14: a <= len fs2 ; :: thesis: Del (fs1 ^ fs2),((len fs1) + a) = fs1 ^ (Del fs2,a)

then A15: a in dom fs2 by A11, FINSEQ_3:27;
A16: (len fs1) + a <= len (fs1 ^ fs2) by A1, A14, XREAL_1:8;
(len fs1) + a >= 1 by A11, NAT_1:12;
then A17: (len fs1) + a in dom (fs1 ^ fs2) by A16, FINSEQ_3:27;
then consider g1, g2 being FinSequence such that
A18: ( fs1 ^ fs2 = (g1 ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2 & len g1 = ((len fs1) + a) - 1 & len g2 = (len (fs1 ^ fs2)) - ((len fs1) + a) ) by Lm41;
A19: Del (fs1 ^ fs2),((len fs1) + a) = g1 ^ g2 by A17, A18, Lm42;
A20: fs1 ^ fs2 = g1 ^ (<*((fs1 ^ fs2) . ((len fs1) + a))*> ^ g2) by A18, FINSEQ_1:45;
a - 1 >= 0 by A11, XREAL_1:50;
then (a - 1) + (len fs1) >= 0 + (len fs1) by XREAL_1:8;
then consider t being FinSequence such that
A21: fs1 ^ t = g1 by A18, A20, FINSEQ_1:64;
fs1 ^ ((t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2) = (fs1 ^ (t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>)) ^ g2 by FINSEQ_1:45
.= fs1 ^ fs2 by A18, A21, FINSEQ_1:45 ;
then A22: fs2 = (t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2 by FINSEQ_1:46;
(len fs1) + (a - 1) = (len fs1) + (len t) by A18, A21, FINSEQ_1:35;
then Del fs2,a = t ^ g2 by A15, A22, Lm42;
hence Del (fs1 ^ fs2),((len fs1) + a) = fs1 ^ (Del fs2,a) by A19, A21, FINSEQ_1:45; :: thesis: verum

end;

end;

end;

hence Del (fs1 ^ fs2),((len fs1) + a) = fs1 ^ (Del fs2,a) ; :: thesis: verum

end;

hence ( ( a <= len fs1 implies Del (fs1 ^ fs2),a = (Del fs1,a) ^ fs2 ) & ( a >= 1 implies Del (fs1 ^ fs2),((len fs1) + a) = fs1 ^ (Del fs2,a) ) ) by A2; :: thesis: verum