let fs be FinSequence; for v being object holds
( Del ((<*v*> ^ fs),1) = fs & Del ((fs ^ <*v*>),((len fs) + 1)) = fs )
let v be object ; ( Del ((<*v*> ^ fs),1) = fs & Del ((fs ^ <*v*>),((len fs) + 1)) = fs )
A1:
len <*v*> = 1
by FINSEQ_1:39;
then
1 in dom <*v*>
by FINSEQ_3:25;
then
(len (Del (<*v*>,1))) + 1 = 1
by A1, Def1;
then A2:
Del (<*v*>,1) = {}
;
( 1 <= len <*v*> & {} ^ fs = fs )
by FINSEQ_1:34, FINSEQ_1:39;
hence
Del ((<*v*> ^ fs),1) = fs
by A2, Lm13; Del ((fs ^ <*v*>),((len fs) + 1)) = fs
fs ^ {} = fs
by FINSEQ_1:34;
hence
Del ((fs ^ <*v*>),((len fs) + 1)) = fs
by A2, Lm13; verum