theorem Th4: :: NOMIN_5:4

for V, A being set
for d1 being NonatomicND of V,A
for i, j being Element of V st A is complex-containing & i in dom d1 & j in dom d1 & d1 in dom (addition (A,i,j)) holds
for x, y being Complex st x = d1 . i & y = d1 . j holds
(addition (A,i,j)) . d1 = x + y