let n, m be Nat; :: thesis: for K being Field
for a being Element of K
for i, j being Nat
for M being Matrix of n,m,K st i in dom M & j in Seg (width M) holds
(a * (Line (M,i))) . j = a * (M * (i,j))
let K be Field; :: thesis: for a being Element of K
for i, j being Nat
for M being Matrix of n,m,K st i in dom M & j in Seg (width M) holds
(a * (Line (M,i))) . j = a * (M * (i,j))
let a be Element of K; :: thesis: for i, j being Nat
for M being Matrix of n,m,K st i in dom M & j in Seg (width M) holds
(a * (Line (M,i))) . j = a * (M * (i,j))
let i, j be Nat; :: thesis: for M being Matrix of n,m,K st i in dom M & j in Seg (width M) holds
(a * (Line (M,i))) . j = a * (M * (i,j))
let M be Matrix of n,m,K; :: thesis: ( i in dom M & j in Seg (width M) implies (a * (Line (M,i))) . j = a * (M * (i,j)) )
assume that
A1: i in dom M and
A2: j in Seg (width M) ; :: thesis: (a * (Line (M,i))) . j = a * (M * (i,j))
A3: [i,j] in Indices M by A1, A2, ZFMISC_1:87;
A4: j in Seg (width (a * M)) by A2, MATRIX_3:def 5;
dom M = Seg (len M) by FINSEQ_1:def 3;
then ( 1 <= i & i <= len M ) by A1, FINSEQ_1:1;
then (a * (Line (M,i))) . j = (Line ((a * M),i)) . j by MATRIXR1:20
.= (a * M) * (i,j) by A4, MATRIX_0:def 7
.= a * (M * (i,j)) by A3, MATRIX_3:def 5 ;
hence (a * (Line (M,i))) . j = a * (M * (i,j)) ; :: thesis: verum