for ra being Element of F_Real
for N being Matrix of 3,F_Real holds ra * N = (ra * (1. (F_Real,3))) * N