let M1, M2 be Matrix of n,m,D; :: thesis: ( ( len pD = width M & len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies M1 * (i,j) = M * (i,j) ) & ( i = l implies M1 * (l,j) = pD . j ) ) ) & len M2 = len M & width M2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies M2 * (i,j) = M * (i,j) ) & ( i = l implies M2 * (l,j) = pD . j ) ) ) implies M1 = M2 ) & ( not len pD = width M & M1 = M & M2 = M implies M1 = M2 ) )
thus ( len pD = width M & len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies M1 * (i,j) = M * (i,j) ) & ( i = l implies M1 * (l,j) = pD . j ) ) ) & len M2 = len M & width M2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies M2 * (i,j) = M * (i,j) ) & ( i = l implies M2 * (l,j) = pD . j ) ) ) implies M1 = M2 ) :: thesis: ( not len pD = width M & M1 = M & M2 = M implies M1 = M2 )

proof

assume len pD = width M ; :: thesis: ( not len M1 = len M or not width M1 = width M or ex i, j being Nat st
( [i,j] in Indices M & not ( ( i <> l implies M1 * (i,j) = M * (i,j) ) & ( i = l implies M1 * (l,j) = pD . j ) ) ) or not len M2 = len M or not width M2 = width M or ex i, j being Nat st
( [i,j] in Indices M & not ( ( i <> l implies M2 * (i,j) = M * (i,j) ) & ( i = l implies M2 * (l,j) = pD . j ) ) ) or M1 = M2 )
assume that
A17: len M1 = len M and
A18: width M1 = width M and
A19: for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies M1 * (i,j) = M * (i,j) ) & ( i = l implies M1 * (l,j) = pD . j ) ) ; :: thesis: ( not len M2 = len M or not width M2 = width M or ex i, j being Nat st
( [i,j] in Indices M & not ( ( i <> l implies M2 * (i,j) = M * (i,j) ) & ( i = l implies M2 * (l,j) = pD . j ) ) ) or M1 = M2 )
assume that
len M2 = len M and
width M2 = width M and
A20: for i, j being Nat st [i,j] in Indices M holds
( ( i <> l implies M2 * (i,j) = M * (i,j) ) & ( i = l implies M2 * (l,j) = pD . j ) ) ; :: thesis: M1 = M2
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = M2 * (i,j)
then A21: [i,j] in Indices M by A17, A18, MATRIX_4:55;
then A22: ( i = l implies M1 * (l,j) = pD . j ) by A19;
A23: ( i <> l implies M2 * (i,j) = M * (i,j) ) by A20, A21;
( i <> l implies M1 * (i,j) = M * (i,j) ) by A19, A21;
hence M1 * (i,j) = M2 * (i,j) by A20, A21, A22, A23; :: thesis: verum

end;

hence M1 = M2 by MATRIX_1:27; :: thesis: verum

end;

thus ( not len pD = width M & M1 = M & M2 = M implies M1 = M2 ) ; :: thesis: verum