theorem Th09: :: PASCAL:9

for p being FinSequence of REAL
for M being Matrix of 3,REAL
for a, b, c, d, e, f, g, h, i, p1, p2, p3 being Element of REAL st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & p = <*p1,p2,p3*> holds
M * p = <*(((a * p1) + (b * p2)) + (c * p3)),(((d * p1) + (e * p2)) + (f * p3)),(((g * p1) + (h * p2)) + (i * p3))*>