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

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