let K be Field; :: thesis: for a being Element of K
for M being Matrix of K
for i being Nat st 1 <= i & i <= len M holds
Line (a * M),i = a * (Line M,i)
let a be Element of K; :: thesis: for M being Matrix of K
for i being Nat st 1 <= i & i <= len M holds
Line (a * M),i = a * (Line M,i)
let M be Matrix of K; :: thesis: for i being Nat st 1 <= i & i <= len M holds
Line (a * M),i = a * (Line M,i)
let i be Nat; :: thesis: ( 1 <= i & i <= len M implies Line (a * M),i = a * (Line M,i) )
assume A1: ( 1 <= i & i <= len M ) ; :: thesis: Line (a * M),i = a * (Line M,i)
A2: len (a * (Line M,i)) = len (Line M,i) by Th16;
A3: len (Line M,i) = width M by MATRIX_1:def 8;
A4: width (a * M) = width M by MATRIX_3:def 5;
then A5: dom (a * (Line M,i)) = Seg (width (a * M)) by A2, A3, FINSEQ_1:def 3;
A6: Seg (width M) = Seg (width (a * M)) by MATRIX_3:def 5;
for j being Nat st j in Seg (width (a * M)) holds
(a * (Line M,i)) . j = (a * M) * i,j

proof

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

end;

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