let p be FinSequence of REAL ; :: thesis: for M being Matrix of 3,REAL st p = 0. (TOP-REAL 3) holds
M * p = p
let M be Matrix of 3,REAL; :: thesis: ( p = 0. (TOP-REAL 3) implies M * p = p )
assume A1: p = 0. (TOP-REAL 3) ; :: thesis: M * p = p
consider a, b, c, d, e, f, g, h, i being Element of REAL such that
A2: MXR2MXF M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> by Th03;
A3: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> by A2, MATRIXR1:def 1;
set u = 0. (TOP-REAL 3);
A4: ( p . 1 = 0 & p . 2 = 0 & p . 3 = 0 ) by A1, EUCLID_5:4, FINSEQ_1:45;
reconsider r1 = p . 1, r2 = p . 2, r3 = p . 3 as Element of REAL by XREAL_0:def 1;
A5: p = <*r1,r2,r3*> by A1, EUCLID_5:4, A4;
M * p = <*(((a * r1) + (b * r2)) + (c * r3)),(((d * r1) + (e * r2)) + (f * r3)),(((g * r1) + (h * r2)) + (i * r3))*> by A3, A5, Th09
.= <*0,0,0*> by A4 ;
hence M * p = p by A1, EUCLID_5:4; :: thesis: verum