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: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 ;
then not (len fs1) + a in dom (fs1 ^ fs2) by FINSEQ_3:25;
hence Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ fs2 by WSIERP_1:def 1
.= fs1 ^ (Del (fs2,a)) by ;
:: 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 ;
a - 1 >= 0 by ;
then A8: (a - 1) + (len fs1) >= 0 + (len fs1) by XREAL_1:6;
A9: (len fs1) + a >= 1 by ;
(len fs1) + a <= len (fs1 ^ fs2) by ;
then A10: (len fs1) + a in dom (fs1 ^ fs2) by ;
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 Lm40;
A13: Del ((fs1 ^ fs2),((len fs1) + a)) = g1 ^ g2 by ;
fs1 ^ fs2 = g1 ^ (<*((fs1 ^ fs2) . ((len fs1) + a))*> ^ g2) by ;
then consider t being FinSequence such that
A14: fs1 ^ t = g1 by ;
fs1 ^ ((t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2) = (fs1 ^ (t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>)) ^ g2 by FINSEQ_1:32
.= fs1 ^ fs2 by ;
then A15: fs2 = (t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2 by FINSEQ_1:33;
(len fs1) + (a - 1) = (len fs1) + (len t) by ;
then Del (fs2,a) = t ^ g2 by ;
hence Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) by ; :: 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 ;
then A17: a <= len (fs1 ^ fs2) by ;
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 ;
hence Del ((fs1 ^ fs2),a) = fs1 ^ fs2 by WSIERP_1:def 1
.= (Del (fs1,a)) ^ fs2 by ;
:: thesis: verum
end;
suppose A20: a >= 1 ; :: thesis: Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2
then A21: a in dom (fs1 ^ fs2) by ;
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 Lm40;
len (g1 ^ <*((fs1 ^ fs2) . a)*>) = (a - 1) + 1 by
.= a ;
then consider t being FinSequence such that
A24: fs1 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ t by ;
(g1 ^ <*((fs1 ^ fs2) . a)*>) ^ g2 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ (t ^ fs2) by ;
then A25: g2 = t ^ fs2 by FINSEQ_1:33;
a in dom fs1 by ;
then A26: Del (fs1,a) = g1 ^ t by ;
thus Del ((fs1 ^ fs2),a) = g1 ^ g2 by
.= (Del (fs1,a)) ^ fs2 by ; :: 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