let a be Real; 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; 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; ( 1 <= i & i <= width M implies Col ((a * M),i) = a * (Col (M,i)) )
assume A1:
( 1 <= i & i <= width M )
; 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; verum