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) by FINSEQ_1:35;

A2: now

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

now

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

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

then A5: not a in dom fs2 by FINSEQ_3:27;
(len fs1) + a > len (fs1 ^ fs2) by A1, A4, 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 A5, WSIERP_1:def 1 ;
:: thesis: verum

end;

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

then A7: a in dom fs2 by A3, FINSEQ_3:27;
a - 1 >= 0 by A3, XREAL_1:50;
then A8: (a - 1) + (len fs1) >= 0 + (len fs1) by XREAL_1:8;
A9: (len fs1) + a >= 1 by A3, NAT_1:12;
(len fs1) + a <= len (fs1 ^ fs2) by A1, A6, XREAL_1:8;
then A10: (len fs1) + a in dom (fs1 ^ fs2) by A9, FINSEQ_3:27;
then consider g1, g2 being FinSequence such that
A11: fs1 ^ fs2 = (g1 ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2 and
A12: len g1 = ((len fs1) + a) - 1 and
len g2 = (len (fs1 ^ fs2)) - ((len fs1) + a) by Lm41;
A13: Del (fs1 ^ fs2),((len fs1) + a) = g1 ^ g2 by A10, A11, A12, Lm42;
fs1 ^ fs2 = g1 ^ (<*((fs1 ^ fs2) . ((len fs1) + a))*> ^ g2) by A11, FINSEQ_1:45;
then consider t being FinSequence such that
A14: fs1 ^ t = g1 by A12, A8, 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 A11, A14, FINSEQ_1:45 ;
then A15: fs2 = (t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2 by FINSEQ_1:46;
(len fs1) + (a - 1) = (len fs1) + (len t) by A12, A14, FINSEQ_1:35;
then Del fs2,a = t ^ g2 by A7, A15, Lm42;
hence Del (fs1 ^ fs2),((len fs1) + a) = fs1 ^ (Del fs2,a) by A13, A14, FINSEQ_1:45; :: thesis: verum

end;

end;

end;

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

end;

now

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

now

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

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

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

end;

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

then A21: a in dom (fs1 ^ fs2) by A17, FINSEQ_3:27;
then consider g1, g2 being FinSequence such that
A22: fs1 ^ fs2 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ g2 and
A23: len g1 = a - 1 and
len g2 = (len (fs1 ^ fs2)) - a by Lm41;
len (g1 ^ <*((fs1 ^ fs2) . a)*>) = (a - 1) + 1 by A23, FINSEQ_2:19
.= a ;
then consider t being FinSequence such that
A24: fs1 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ t by A16, A22, FINSEQ_1:64;
(g1 ^ <*((fs1 ^ fs2) . a)*>) ^ g2 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ (t ^ fs2) by A22, A24, FINSEQ_1:45;
then A25: g2 = t ^ fs2 by FINSEQ_1:46;
a in dom fs1 by A16, A20, FINSEQ_3:27;
then A26: Del fs1,a = g1 ^ t by A23, A24, Lm42;
thus Del (fs1 ^ fs2),a = g1 ^ g2 by A21, A22, A23, Lm42
.= (Del fs1,a) ^ fs2 by A26, A25, FINSEQ_1:45 ; :: thesis: verum

end;

end;

end;

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