theorem :: BKMODEL1:66

for NR, MR being Matrix of 3,REAL
for p1, p2, p3 being FinSequence of REAL st p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & NR * p1 = MR * p1 & NR * p2 = MR * p2 & NR * p3 = MR * p3 holds
NR = MR