A4: width M = m by A2, MATRIX_1:24;
then A5: len (M @ ) = m by A3, MATRIX_2:12;
A6: len M = n by A2, MATRIX_1:24;
then width (M @ ) = n by A3, A4, MATRIX_2:12;
then M @ is Matrix of m,n,K by A3, A5, MATRIX_1:20;
then consider M1 being Matrix of m,n,K such that
A7: M1 = M @ ;
A8: width (ScalarXLine M1,l,a) = n by A3, MATRIX_1:24;
then A9: len ((ScalarXLine M1,l,a) @ ) = n by A2, MATRIX_2:12;
len (ScalarXLine M1,l,a) = m by A3, MATRIX_1:24;
then width ((ScalarXLine M1,l,a) @ ) = m by A2, A8, MATRIX_2:12;
then (ScalarXLine M1,l,a) @ is Matrix of n,m,K by A2, A9, MATRIX_1:20;
then consider M2 being Matrix of n,m,K such that
A10: M2 = (ScalarXLine M1,l,a) @ ;
take M2 ; :: thesis: ( len M2 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M2 * i,j = a * (M * i,l) ) & ( j <> l implies M2 * i,j = M * i,j ) ) ) )
for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M2 * i,j = a * (M * i,l) ) & ( j <> l implies M2 * i,j = M * i,j ) )

proof

let i, j be Nat; :: thesis: ( i in dom M & j in Seg (width M) implies ( ( j = l implies M2 * i,j = a * (M * i,l) ) & ( j <> l implies M2 * i,j = M * i,j ) ) )
assume that
A11: i in dom M and
A12: j in Seg (width M) ; :: thesis: ( ( j = l implies M2 * i,j = a * (M * i,l) ) & ( j <> l implies M2 * i,j = M * i,j ) )
A13: [i,j] in Indices M by A11, A12, ZFMISC_1:106;
then A14: [j,i] in Indices M1 by A7, MATRIX_1:def 7;
dom (ScalarXLine M1,l,a) = Seg (len (ScalarXLine M1,l,a)) by FINSEQ_1:def 3
.= Seg (len M1) by Def2
.= dom M1 by FINSEQ_1:def 3 ;
then A15: [j,i] in Indices (ScalarXLine M1,l,a) by A14, Th1;
A16: ( j in dom M1 & i in Seg (width M1) ) by A14, ZFMISC_1:106;
thus ( j = l implies M2 * i,j = a * (M * i,l) ) :: thesis: ( j <> l implies M2 * i,j = M * i,j )

proof

A17: [i,l] in Indices M by A1, A11, ZFMISC_1:106;
assume A18: j = l ; :: thesis: M2 * i,j = a * (M * i,l)
M2 * i,j = (ScalarXLine M1,l,a) * j,i by A10, A15, MATRIX_1:def 7
.= a * (M1 * l,i) by A16, A18, Def2
.= a * (M * i,l) by A7, A17, MATRIX_1:def 7 ;
hence M2 * i,j = a * (M * i,l) ; :: thesis: verum

end;

thus ( j <> l implies M2 * i,j = M * i,j ) :: thesis: verum

proof

assume A19: j <> l ; :: thesis: M2 * i,j = M * i,j
M2 * i,j = (ScalarXLine M1,l,a) * j,i by A10, A15, MATRIX_1:def 7
.= M1 * j,i by A16, A19, Def2
.= M * i,j by A7, A13, MATRIX_1:def 7 ;
hence M2 * i,j = M * i,j ; :: thesis: verum

end;

end;

hence ( len M2 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M2 * i,j = a * (M * i,l) ) & ( j <> l implies M2 * i,j = M * i,j ) ) ) ) by A2, A6, MATRIX_1:24; :: thesis: verum