theorem :: WSIERP_1:39

for a being Nat
for fs being FinSequence holds dom (Del (fs,a)) c= dom fs by Lm12;