let m, n be Nat; :: thesis: for K being Field
for a being Element of K
for l being Nat
for M, M1 being Matrix of n,m,K
for pK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line M,l & M1 = RLine M,l,(a * pK) holds
( ( i = l implies M1 * i,j = a * (M * l,j) ) & ( i <> l implies M1 * i,j = M * i,j ) )
let K be Field; :: thesis: for a being Element of K
for l being Nat
for M, M1 being Matrix of n,m,K
for pK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line M,l & M1 = RLine M,l,(a * pK) holds
( ( i = l implies M1 * i,j = a * (M * l,j) ) & ( i <> l implies M1 * i,j = M * i,j ) )
let a be Element of K; :: thesis: for l being Nat
for M, M1 being Matrix of n,m,K
for pK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line M,l & M1 = RLine M,l,(a * pK) holds
( ( i = l implies M1 * i,j = a * (M * l,j) ) & ( i <> l implies M1 * i,j = M * i,j ) )
let l be Nat; :: thesis: for M, M1 being Matrix of n,m,K
for pK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line M,l & M1 = RLine M,l,(a * pK) holds
( ( i = l implies M1 * i,j = a * (M * l,j) ) & ( i <> l implies M1 * i,j = M * i,j ) )
let M, M1 be Matrix of n,m,K; :: thesis: for pK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line M,l & M1 = RLine M,l,(a * pK) holds
( ( i = l implies M1 * i,j = a * (M * l,j) ) & ( i <> l implies M1 * i,j = M * i,j ) )
let pK be FinSequence of K; :: thesis: for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line M,l & M1 = RLine M,l,(a * pK) holds
( ( i = l implies M1 * i,j = a * (M * l,j) ) & ( i <> l implies M1 * i,j = M * i,j ) )
let i, j be Nat; :: thesis: ( i in Seg n & j in Seg (width M) & pK = Line M,l & M1 = RLine M,l,(a * pK) implies ( ( i = l implies M1 * i,j = a * (M * l,j) ) & ( i <> l implies M1 * i,j = M * i,j ) ) )
assume that
A1: i in Seg n and
A2: j in Seg (width M) and
A3: pK = Line M,l and
A4: M1 = RLine M,l,(a * pK) ; :: thesis: ( ( i = l implies M1 * i,j = a * (M * l,j) ) & ( i <> l implies M1 * i,j = M * i,j ) )
thus ( i = l implies M1 * i,j = a * (M * l,j) ) :: thesis: ( i <> l implies M1 * i,j = M * i,j )

proof

assume A5: i = l ; :: thesis: M1 * i,j = a * (M * l,j)
len M = n by MATRIX_1:def 3;
then A6: l in dom M by A1, A5, FINSEQ_1:def 3;
A7: len (a * (Line M,l)) = width M by FINSEQ_1:def 18;
then width M1 = width M by A3, A4, MATRIX11:def 3;
then M1 * i,j = (Line M1,i) . j by A2, MATRIX_1:def 8
.= (a * (Line M,l)) . j by A1, A3, A4, A5, A7, MATRIX11:28
.= a * (M * l,j) by A2, A6, Th3 ;
hence M1 * i,j = a * (M * l,j) ; :: thesis: verum

end;

assume A8: i <> l ; :: thesis: M1 * i,j = M * i,j
len (a * (Line M,l)) = width M by FINSEQ_1:def 18;
then width M1 = width M by A3, A4, MATRIX11:def 3;
hence M1 * i,j = (Line M1,i) . j by A2, MATRIX_1:def 8
.= (Line M,i) . j by A1, A4, A8, MATRIX11:28
.= M * i,j by A2, MATRIX_1:def 8 ;
:: thesis: verum