(len f) |-> 0 = 0 (#) f by EMP;
then reconsider g = (len f) |-> 0 as empty-yielding dom f -defined total complex-valued Function ;
reconsider h = 1 (#) f as dom f -defined total complex-valued Function ;
h + g = h ;
hence f + ((len f) |-> 0) = f ; :: thesis: verum