theorem Th08: :: PASCAL:8

for M being Matrix of 3,F_Real
for a, b, c, d, e, f, g, h, i, x, y, z being Element of F_Real
for v being Element of (TOP-REAL 3)
for uf being FinSequence of F_Real
for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & uf = <*x,y,z*> holds
( p = <*<*(((a * x) + (b * y)) + (c * z))*>,<*(((d * x) + (e * y)) + (f * z))*>,<*(((g * x) + (h * y)) + (i * z))*>*> & v = <*(((a * x) + (b * y)) + (c * z)),(((d * x) + (e * y)) + (f * z)),(((g * x) + (h * y)) + (i * z))*> )