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