let l, n, m, i be Nat; :: thesis: for K being comRing
for a being Element of K
for M, M1 being Matrix of n,m,K st l in dom M & i in dom M & M1 = ScalarXLine (M,l,a) holds
( ( i = l implies Line (M1,i) = a * (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) )
let K be comRing; :: thesis: for a being Element of K
for M, M1 being Matrix of n,m,K st l in dom M & i in dom M & M1 = ScalarXLine (M,l,a) holds
( ( i = l implies Line (M1,i) = a * (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) )
let a be Element of K; :: thesis: for M, M1 being Matrix of n,m,K st l in dom M & i in dom M & M1 = ScalarXLine (M,l,a) holds
( ( i = l implies Line (M1,i) = a * (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) )
let M, M1 be Matrix of n,m,K; :: thesis: ( l in dom M & i in dom M & M1 = ScalarXLine (M,l,a) implies ( ( i = l implies Line (M1,i) = a * (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) ) )
assume that
A1: l in dom M and
A2: i in dom M and
A3: M1 = ScalarXLine (M,l,a) ; :: thesis: ( ( i = l implies Line (M1,i) = a * (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) )
thus ( i = l implies Line (M1,i) = a * (Line (M,l)) ) :: thesis: ( i <> l implies Line (M1,i) = Line (M,i) )

proof

A4: width M1 = width M by Th1;
A5: len (Line (M1,i)) = width M1 by MATRIX_0:def 7;
assume A6: i = l ; :: thesis: Line (M1,i) = a * (Line (M,l))

A7: now :: thesis: for j being Nat st 1 <= j & j <= len (Line (M1,i)) holds
(Line (M1,i)) . j = (a * (Line (M,l))) . j

let j be Nat; :: thesis: ( 1 <= j & j <= len (Line (M1,i)) implies (Line (M1,i)) . j = (a * (Line (M,l))) . j )
assume A8: ( 1 <= j & j <= len (Line (M1,i)) ) ; :: thesis: (Line (M1,i)) . j = (a * (Line (M,l))) . j
A9: j in Seg (width M1) by A5, A8;
hence (Line (M1,i)) . j = M1 * (i,j) by MATRIX_0:def 7
.= a * (M * (l,j)) by A1, A3, A6, A4, A9, Def2
.= (a * (Line (M,l))) . j by A1, A4, A9, Th3 ;
:: thesis: verum

end;

( len (a * (Line (M,l))) = len (Line (M,l)) & len (Line (M,l)) = width M ) by MATRIXR1:16, MATRIX_0:def 7;
hence Line (M1,i) = a * (Line (M,l)) by A5, A7, Th1; :: thesis: verum

end;

A10: len (Line (M1,i)) = width M1 by MATRIX_0:def 7;
A11: width M1 = width M by Th1;
assume A12: i <> l ; :: thesis: Line (M1,i) = Line (M,i)

A13: now :: thesis: for j being Nat st 1 <= j & j <= len (Line (M1,i)) holds
(Line (M1,i)) . j = (Line (M,i)) . j

let j be Nat; :: thesis: ( 1 <= j & j <= len (Line (M1,i)) implies (Line (M1,i)) . j = (Line (M,i)) . j )
assume A14: ( 1 <= j & j <= len (Line (M1,i)) ) ; :: thesis: (Line (M1,i)) . j = (Line (M,i)) . j
A15: j in Seg (width M1) by A10, A14;
hence (Line (M1,i)) . j = M1 * (i,j) by MATRIX_0:def 7
.= M * (i,j) by A2, A3, A12, A11, A15, Def2
.= (Line (M,i)) . j by A11, A15, MATRIX_0:def 7 ;
:: thesis: verum

end;

len (Line (M,i)) = width M by MATRIX_0:def 7;
hence Line (M1,i) = Line (M,i) by A10, A13, Th1; :: thesis: verum