let p be FinSequence of REAL ; for M being Matrix of 3,REAL st p = 0. (TOP-REAL 3) holds
M * p = p
let M be Matrix of 3,REAL; ( p = 0. (TOP-REAL 3) implies M * p = p )
assume A1:
p = 0. (TOP-REAL 3)
; 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; verum