let a be Real; :: thesis: for M being Matrix of REAL
for i being Nat st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
let M be Matrix of REAL; :: thesis: for i being Nat st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
reconsider ea = a as Element of F_Real by XREAL_0:def 1;
let i be Nat; :: thesis: ( 1 <= i & i <= width M implies Col ((a * M),i) = a * (Col (M,i)) )
assume A1: ( 1 <= i & i <= width M ) ; :: thesis: Col ((a * M),i) = a * (Col (M,i))
Col ((a * M),i) = Col ((MXF2MXR (ea * (MXR2MXF M))),i) by Def7
.= ea * (Col ((MXR2MXF M),i)) by A1, Th19 ;
hence Col ((a * M),i) = a * (Col (M,i)) by Th17; :: thesis: verum