let m, n 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 A1: ( i in dom M & j in Seg (width M) ) ; :: thesis: (a * (Line M,i)) . j = a * (M * i,j)
dom M = Seg (len M) by FINSEQ_1:def 3;
then A2: ( 1 <= i & i <= len M ) by A1, FINSEQ_1:3;
A3: [i,j] in Indices M by A1, ZFMISC_1:106;
A4: j in Seg (width (a * M)) by A1, MATRIX_3:def 5;
(a * (Line M,i)) . j = (Line (a * M),i) . j by A2, MATRIXR1:20
.= (a * M) * i,j by A4, MATRIX_1:def 8
.= a * (M * i,j) by A3, MATRIX_3:def 5 ;
hence (a * (Line M,i)) . j = a * (M * i,j) ; :: thesis: verum