theorem :: ANPROJ_8:4

for a, b, c being Real holds <*<*a*>,<*b*>,<*c*>*> is Matrix of 3,1,F_Real