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 & a <> 0. K & 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 & a <> 0. K & 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 & a <> 0. K & 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 & a <> 0. K & 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 A1: ( l in dom M & i in dom M & a <> 0. K & 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

assume A2: i = l ; :: thesis: Line M1,i = a * (Line M,l)
A3: width M1 = width M by Th1;
A4: len (a * (Line M,l)) = len (Line M,l) by MATRIXR1:16;
A5: ( len (Line M1,i) = width M1 & len (Line M,l) = width M ) by MATRIX_1:def 8;

now

let j be Nat; :: thesis: ( 1 <= j & j <= len (Line M1,i) implies (Line M1,i) . j = (a * (Line M,l)) . j )
assume A6: ( 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 A7: j in Seg (width M1) by A5, A6;
hence (Line M1,i) . j = M1 * i,j by MATRIX_1:def 8
.= a * (M * l,j) by A1, A2, A3, A7, Def2
.= (a * (Line M,l)) . j by A1, A3, A7, Th3 ;
:: thesis: verum

end;

hence Line M1,i = a * (Line M,l) by A3, A4, A5, FINSEQ_1:18; :: thesis: verum

end;

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

now

let j be Nat; :: thesis: ( 1 <= j & j <= len (Line M1,i) implies (Line M1,i) . j = (Line M,i) . j )
assume A11: ( 1 <= j & j <= len (Line M1,i) ) ; :: thesis: (Line M1,i) . j = (Line M,i) . j
j in NAT by ORDINAL1:def 13;
then A12: j in Seg (width M1) by A10, A11;
hence (Line M1,i) . j = M1 * i,j by MATRIX_1:def 8
.= M * i,j by A1, A8, A9, A12, Def2
.= (Line M,i) . j by A9, A12, MATRIX_1:def 8 ;
:: thesis: verum

end;

hence Line M1,i = Line M,i by A9, A10, FINSEQ_1:18; :: thesis: verum