theorem Th5: :: NOMIN_5:5

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 (multiplication (A,i,j)) holds
for x, y being Complex st x = d1 . i & y = d1 . j holds
(multiplication (A,i,j)) . d1 = x * y