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