theorem :: NOMIN_4:15

for V, A being set
for d1 being NonatomicND of V,A
for a, b being Element of V st A is complex-containing & a in dom d1 & b in dom d1 & d1 in dom (subtraction (A,a,b)) holds
for x, y being Complex st x = d1 . a & y = d1 . b holds
(subtraction (A,a,b)) . d1 = x - y