let l, n, m, i be Nat; :: thesis:
let K be Field; :: thesis:
let a be Element of K; :: thesis:
let M, M1 be Matrix of n,m,K; :: thesis:
assume that
A1: l in dom M and
A2: i in dom M and
A3: M1 = ScalarXLine (M,l,a) ; :: thesis:
thus ( i = l implies Line (M1,i) = a * (Line (M,l)) ) :: thesis:

let j be Nat; :: thesis:
assume A8: ( 1 <= j & j <= len (Line (M1,i)) ) ; :: thesis:
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:

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:

end;

let j be Nat; :: thesis:
assume A14: ( 1 <= j & j <= len (Line (M1,i)) ) ; :: thesis:
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:

end;