for M being non empty set
for V being ComplexNormSpace
for f1 being PartFunc of M,COMPLEX
for f2 being PartFunc of M,V holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)}))