let a be 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:22;

A2: now :: thesis: ( a >= 1 implies Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) )

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 :: thesis: Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a))

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:25;
(len fs1) + a > len (fs1 ^ fs2) by A1, A4, XREAL_1:6;
then not (len fs1) + a in dom (fs1 ^ fs2) by FINSEQ_3:25;
hence Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ fs2 by Def1
.= fs1 ^ (Del (fs2,a)) by A5, Def1 ;
:: 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:25;
a - 1 >= 0 by A3, XREAL_1:48;
then A8: (len fs1) + (a - 1) >= len fs1 by Lm1;
A9: (len fs1) + a >= 1 by A3, NAT_1:12;
(len fs1) + a <= len (fs1 ^ fs2) by A1, A6, XREAL_1:6;
then A10: (len fs1) + a in dom (fs1 ^ fs2) by A9, FINSEQ_3:25;
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 Lm10;
A13: Del ((fs1 ^ fs2),((len fs1) + a)) = g1 ^ g2 by A10, A11, A12, Lm11;
fs1 ^ fs2 = g1 ^ (<*((fs1 ^ fs2) . ((len fs1) + a))*> ^ g2) by A11, FINSEQ_1:32;
then consider t being FinSequence such that
A14: fs1 ^ t = g1 by A12, A8, FINSEQ_1:47;
fs1 ^ ((t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2) = (fs1 ^ (t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>)) ^ g2 by FINSEQ_1:32
.= fs1 ^ fs2 by A11, A14, FINSEQ_1:32 ;
then A15: fs2 = (t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2 by FINSEQ_1:33;
(len fs1) + (a - 1) = (len fs1) + (len t) by A12, A14, FINSEQ_1:22;
then Del (fs2,a) = t ^ g2 by A7, A15, Lm11;
hence Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) by A13, A14, FINSEQ_1:32; :: thesis: verum

end;

end;

end;

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

end;

now :: thesis: ( a <= len fs1 implies Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 )

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

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:25;
not a in dom (fs1 ^ fs2) by A18, FINSEQ_3:25;
hence Del ((fs1 ^ fs2),a) = fs1 ^ fs2 by Def1
.= (Del (fs1,a)) ^ fs2 by A19, Def1 ;
:: 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:25;
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 Lm10;
len (g1 ^ <*((fs1 ^ fs2) . a)*>) = (a - 1) + 1 by A23, FINSEQ_2:16
.= a ;
then consider t being FinSequence such that
A24: fs1 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ t by A16, A22, FINSEQ_1:47;
(g1 ^ <*((fs1 ^ fs2) . a)*>) ^ g2 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ (t ^ fs2) by A22, A24, FINSEQ_1:32;
then A25: g2 = t ^ fs2 by FINSEQ_1:33;
a in dom fs1 by A16, A20, FINSEQ_3:25;
then A26: Del (fs1,a) = g1 ^ t by A23, A24, Lm11;
thus Del ((fs1 ^ fs2),a) = g1 ^ g2 by A21, A22, A23, Lm11
.= (Del (fs1,a)) ^ fs2 by A26, A25, FINSEQ_1:32 ; :: 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