theorem Th75: :: ANPROJ_8:92

for R being Ring
for pf being FinSequence of R
for N being Matrix of 3,R st len pf = 3 holds
( Line ((N * (<*pf*> @)),1) = <*((N * (<*pf*> @)) * (1,1))*> & Line ((N * (<*pf*> @)),2) = <*((N * (<*pf*> @)) * (2,1))*> & Line ((N * (<*pf*> @)),3) = <*((N * (<*pf*> @)) * (3,1))*> )