theorem Th5: :: ANPROJ_8:6

for K being non empty multMagma
for a1, a2, a3, b1, b2, b3 being Element of K holds mlt (<*a1,a2,a3*>,<*b1,b2,b3*>) = <*(a1 * b1),(a2 * b2),(a3 * b3)*>