reconsider af = abs f as len f -element real-valued FinSequence ;
f null f is len f -element FinSequence ;
then reconsider g = f + (abs 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 delneg f is len f -element ; :: thesis: verum