let i be Nat; :: thesis: for K being Field
for a being Element of K
for M being Matrix of K st 1 <= i & i <= width M holds
Col (a * M),i = a * (Col M,i)
let K be Field; :: thesis: for a being Element of K
for M being Matrix of K st 1 <= i & i <= width M holds
Col (a * M),i = a * (Col M,i)
let a be Element of K; :: thesis: for M being Matrix of K st 1 <= i & i <= width M holds
Col (a * M),i = a * (Col M,i)
let M be Matrix of K; :: 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)
A2: len (a * (Col M,i)) = len (Col M,i) by Th16;
A3: len (Col M,i) = len M by MATRIX_1:def 9;
A4: len (a * M) = len M by MATRIX_3:def 5;
then A5: dom (a * (Col M,i)) = Seg (len (a * M)) by A2, A3, FINSEQ_1:def 3;
A6: Seg (len (a * M)) = dom (a * M) by FINSEQ_1:def 3;
A7: dom M = dom (a * M) by A4, FINSEQ_3:31;
for j being Nat st j in dom (a * M) holds
(a * (Col M,i)) . j = (a * M) * j,i

proof

let j be Nat; :: thesis: ( j in dom (a * M) implies (a * (Col M,i)) . j = (a * M) * j,i )
assume A8: j in dom (a * M) ; :: thesis: (a * (Col M,i)) . j = (a * M) * j,i
i in Seg (width M) by A1, FINSEQ_1:3;
then [j,i] in Indices M by A7, A8, ZFMISC_1:106;
then A9: (a * M) * j,i = a * (M * j,i) by MATRIX_3:def 5;
(Col M,i) . j = M * j,i by A7, A8, MATRIX_1:def 9;
hence (a * (Col M,i)) . j = (a * M) * j,i by A5, A6, A8, A9, FVSUM_1:62; :: thesis: verum

end;

hence Col (a * M),i = a * (Col M,i) by A2, A3, A4, MATRIX_1:def 9; :: thesis: verum