let fs be FinSequence; :: thesis: for v being object holds
( Del ((<*v*> ^ fs),1) = fs & Del ((fs ^ <*v*>),((len fs) + 1)) = fs )
let v be object ; :: thesis: ( 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; :: thesis: Del ((fs ^ <*v*>),((len fs) + 1)) = fs
fs ^ {} = fs by FINSEQ_1:34;
hence Del ((fs ^ <*v*>),((len fs) + 1)) = fs by A2, Lm13; :: thesis: verum