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 ;
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