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;
A2: 1 <= len <*v*> by FINSEQ_1:56;
A3: Del <*v*>,1 = {}

proof

1 in dom <*v*> by A1, FINSEQ_3:27;
then (len (Del <*v*>,1)) + 1 = 1 by A1, Def1;
hence Del <*v*>,1 = {} ; :: thesis: verum

end;

A4: ( fs ^ {} = fs & {} ^ fs = fs ) by FINSEQ_1:47;
hence Del (<*v*> ^ fs),1 = fs by A2, A3, Lm15; :: thesis: Del (fs ^ <*v*>),((len fs) + 1) = fs
thus Del (fs ^ <*v*>),((len fs) + 1) = fs by A3, A4, Lm15; :: thesis: verum