let M1, M2 be Matrix of n,m,K; ( len M1 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) ) ) & len M2 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies M2 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M2 * (i,j) = M * (i,j) ) ) ) implies M1 = M2 )
assume that
len M1 = len M
and
A2:
for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )
and
len M2 = len M
and
A3:
for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( i = l implies M2 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M2 * (i,j) = M * (i,j) ) )
; M1 = M2
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)
proof
A4:
Indices M = Indices M1
by MATRIX_0:26;
let i,
j be
Nat;
( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume
[i,j] in Indices M1
;
M1 * (i,j) = M2 * (i,j)
then A5:
(
i in dom M &
j in Seg (width M) )
by A4, ZFMISC_1:87;
then A6:
(
i <> l implies
M1 * (
i,
j)
= M * (
i,
j) )
by A2;
(
i = l implies
M1 * (
i,
j)
= a * (M * (l,j)) )
by A2, A5;
hence
M1 * (
i,
j)
= M2 * (
i,
j)
by A3, A5, A6;
verum
end;
hence
M1 = M2
by MATRIX_0:27; verum