A2: ( len M = n & width M = m ) by A1, MATRIX_1:24;
then ( len (M @ ) = m & width (M @ ) = n ) by A1, MATRIX_2:12;
then M @ is Matrix of m,n,K by A1, MATRIX_1:20;
then consider M1 being Matrix of m,n,K such that
A3: M1 = M @ ;
( len (RlineXScalar M1,l,k,a) = m & width (RlineXScalar M1,l,k,a) = n ) by A1, MATRIX_1:24;
then ( len ((RlineXScalar M1,l,k,a) @ ) = n & width ((RlineXScalar M1,l,k,a) @ ) = m ) by A1, MATRIX_2:12;
then (RlineXScalar M1,l,k,a) @ is Matrix of n,m,K by A1, MATRIX_1:20;
then consider M2 being Matrix of n,m,K such that
A4: M2 = (RlineXScalar M1,l,k,a) @ ;
A5: 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,k)) + (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,k)) + (M * i,l) ) & ( j <> l implies M2 * i,j = M * i,j ) ) )
assume A6: ( i in dom M & j in Seg (width M) ) ; :: thesis: ( ( j = l implies M2 * i,j = (a * (M * i,k)) + (M * i,l) ) & ( j <> l implies M2 * i,j = M * i,j ) )
len M1 = width M by A3, MATRIX_1:def 7;
then A7: ( l in dom M1 & k in dom M1 ) by A1, FINSEQ_1:def 3;
A8: [i,j] in Indices M by A6, ZFMISC_1:106;
then A9: [j,i] in Indices M1 by A3, MATRIX_1:def 7;
then A10: ( j in dom M1 & i in Seg (width M1) ) by ZFMISC_1:106;
dom (RlineXScalar M1,l,k,a) = Seg (len (RlineXScalar M1,l,k,a)) by FINSEQ_1:def 3
.= Seg (len M1) by A7, Def3
.= dom M1 by FINSEQ_1:def 3 ;
then A11: [j,i] in Indices (RlineXScalar M1,l,k,a) by A9, Th1;
thus ( j = l implies M2 * i,j = (a * (M * i,k)) + (M * i,l) ) :: thesis: ( j <> l implies M2 * i,j = M * i,j )

proof

assume A12: j = l ; :: thesis: M2 * i,j = (a * (M * i,k)) + (M * i,l)
A13: [i,l] in Indices M by A1, A6, ZFMISC_1:106;
A14: [i,k] in Indices M by A1, A6, ZFMISC_1:106;
M2 * i,j = (RlineXScalar M1,l,k,a) * j,i by A4, A11, MATRIX_1:def 7
.= (a * (M1 * k,i)) + (M1 * l,i) by A7, A10, A12, Def3
.= (a * (M * i,k)) + (M1 * l,i) by A3, A14, MATRIX_1:def 7
.= (a * (M * i,k)) + (M * i,l) by A3, A13, MATRIX_1:def 7 ;
hence M2 * i,j = (a * (M * i,k)) + (M * i,l) ; :: thesis: verum

end;

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

proof

assume A15: j <> l ; :: thesis: M2 * i,j = M * i,j
M2 * i,j = (RlineXScalar M1,l,k,a) * j,i by A4, A11, MATRIX_1:def 7
.= M1 * j,i by A7, A10, A15, Def3
.= M * i,j by A3, A8, MATRIX_1:def 7 ;
hence M2 * i,j = M * i,j ; :: thesis: verum

end;

end;

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,k)) + (M * i,l) ) & ( j <> l implies M2 * i,j = M * i,j ) ) ) )
thus ( 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,k)) + (M * i,l) ) & ( j <> l implies M2 * i,j = M * i,j ) ) ) ) by A1, A2, A5, MATRIX_1:24; :: thesis: verum