reconsider af = abs f as len f -element real-valued FinSequence ;
f null f is len f -element FinSequence ;
then reconsider g = (abs f) - f as len f -element complex-valued FinSequence ;
reconsider h = (1 / 2) (#) g as len f -element FinSequence ;
h null f is len f -element ;
hence delpos f is len f -element ; :: thesis: verum