f = (len f) |-> 0 ;
hence Sum f is zero ; :: thesis: verum