let ra be Element of F_Real; :: thesis: for N being Matrix of 3,F_Real holds ra * N = (ra * (1. (F_Real,3))) * N
let N be Matrix of 3,F_Real; :: thesis: ra * N = (ra * (1. (F_Real,3))) * N
width (1. (F_Real,3)) = 3 by MATRIX_0:24;
then A1: width (1. (F_Real,3)) = len N by MATRIX_0:24;
ra * N = ra * ((1. (F_Real,3)) * N) by MATRIX_3:18;
hence ra * N = (ra * (1. (F_Real,3))) * N by A1, MATRIX15:1; :: thesis: verum