theorem :: WSIERP_1:40

for fs being FinSequence
for v being object holds
( Del ((<*v*> ^ fs),1) = fs & Del ((fs ^ <*v*>),((len fs) + 1)) = fs ) by Lm14;