A1: dom (delpos f) = dom f by DMN
.= dom (delall f) by DMN ;
for k being object st k in dom (delall f) holds
(delpos f) . k = (delall f) . k ;
hence delpos f = delall f by A1, FUNCT_1:2; :: thesis: verum