let n, m, l, i be Nat; :: thesis: for K being Field
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 Field; :: 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_1:def 8;
assume A6: i = l ; :: thesis: Line M1,i = a * (Line M,l)

A7: now

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
j in NAT by ORDINAL1:def 13;
then A9: j in Seg (width M1) by A5, A8;
hence (Line M1,i) . j = M1 * i,j by MATRIX_1:def 8
.= 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_1:def 8;
hence Line M1,i = a * (Line M,l) by A5, A7, Th1, FINSEQ_1:18; :: thesis: verum

end;

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

A13: now

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
j in NAT by ORDINAL1:def 13;
then A15: j in Seg (width M1) by A10, A14;
hence (Line M1,i) . j = M1 * i,j by MATRIX_1:def 8
.= M * i,j by A2, A3, A12, A11, A15, Def2
.= (Line M,i) . j by A11, A15, MATRIX_1:def 8 ;
:: thesis: verum

end;

len (Line M,i) = width M by MATRIX_1:def 8;
hence Line M1,i = Line M,i by A10, A13, Th1, FINSEQ_1:18; :: thesis: verum