let K be non empty multMagma ; :: 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: width (a * M) = width M by MATRIX_3:def 5;
A3: Seg (width M) = Seg (width (a * M)) by MATRIX_3:def 5;
A4: ( len (a * (Line (M,i))) = len (Line (M,i)) & len (Line (M,i)) = width M ) by Th16, MATRIX_0:def 7;
then A5: dom (a * (Line (M,i))) = Seg (width (a * M)) by A2, FINSEQ_1:def 3;
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 A6: j in Seg (width (a * M)) ; :: thesis: (a * (Line (M,i))) . j = (a * M) * (i,j)
i in dom M by A1, FINSEQ_3:25;
then [i,j] in Indices M by A3, A6, ZFMISC_1:87;
then A7: (a * M) * (i,j) = a * (M * (i,j)) by MATRIX_3:def 5;
(Line (M,i)) . j = M * (i,j) by A3, A6, MATRIX_0:def 7;
hence (a * (Line (M,i))) . j = (a * M) * (i,j) by A5, A6, A7, FVSUM_1:50; :: thesis: verum

end;

hence Line ((a * M),i) = a * (Line (M,i)) by A4, A2, MATRIX_0:def 7; :: thesis: verum