theorem Th08: :: ANPROJ_9:7

for a11, a12, a13, a21, a22, a23, a31, a32, a33, b1, b2, b3 being Element of F_Real
for A being Matrix of 3,3,F_Real
for B being Matrix of 3,1,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b1*>,<*b2*>,<*b3*>*> holds
A * B = <*<*(((a11 * b1) + (a12 * b2)) + (a13 * b3))*>,<*(((a21 * b1) + (a22 * b2)) + (a23 * b3))*>,<*(((a31 * b1) + (a32 * b2)) + (a33 * b3))*>*>