let f be complex-valued Function; :: thesis: f + ((dom f) --> 0) = f
thus f + ((dom f) --> 0) = f + 0 by Th3
.= f ; :: thesis: verum