let n, m, l, i, j be Nat; :: thesis: for K being non empty multMagma
for a being Element of K
for M, M1 being Matrix of n,m,K
for pK being FinSequence of K 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 non empty multMagma ; :: thesis: for a being Element of K
for M, M1 being Matrix of n,m,K
for pK being FinSequence of K 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 M, M1 being Matrix of n,m,K
for pK being FinSequence of K 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 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: ( 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_0:def 2;
then A6: l in dom M by A1, A5, FINSEQ_1:def 3;
A7: len (a * (Line (M,l))) = width M by CARD_1:def 7;
then width M1 = width M by A3, A4, MATRIX11:def 3;
then M1 * (i,j) = (Line (M1,i)) . j by A2, MATRIX_0:def 7
.= (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 CARD_1:def 7;
then width M1 = width M by A3, A4, MATRIX11:def 3;
hence M1 * (i,j) = (Line (M1,i)) . j by A2, MATRIX_0:def 7
.= (Line (M,i)) . j by A1, A4, A8, MATRIX11:28
.= M * (i,j) by A2, MATRIX_0:def 7 ;
:: thesis: verum