theorem Th7: :: ANPROJ_8:8
for M being Matrix of 3,F_Real
for N being Matrix of 3,1,F_Real st N = <*<*0*>,<*0*>,<*0*>*> holds
M * N = <*<*0*>,<*0*>,<*0*>*>