let M1, M2 be Matrix of n,m,D; ( ( len pD = len M & len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( j <> c implies M1 * (i,j) = M * (i,j) ) & ( j = c implies M1 * (i,c) = pD . i ) ) ) & len M2 = len M & width M2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( j <> c implies M2 * (i,j) = M * (i,j) ) & ( j = c implies M2 * (i,c) = pD . i ) ) ) implies M1 = M2 ) & ( not len pD = len M & M1 = M & M2 = M implies M1 = M2 ) )
thus
( len pD = len M & len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( j <> c implies M1 * (i,j) = M * (i,j) ) & ( j = c implies M1 * (i,c) = pD . i ) ) ) & len M2 = len M & width M2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( j <> c implies M2 * (i,j) = M * (i,j) ) & ( j = c implies M2 * (i,c) = pD . i ) ) ) implies M1 = M2 )
( not len pD = len M & M1 = M & M2 = M implies M1 = M2 )proof
assume
len pD = len M
;
( not len M1 = len M or not width M1 = width M or ex i, j being Nat st
( [i,j] in Indices M & not ( ( j <> c implies M1 * (i,j) = M * (i,j) ) & ( j = c implies M1 * (i,c) = pD . i ) ) ) 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 ( ( j <> c implies M2 * (i,j) = M * (i,j) ) & ( j = c implies M2 * (i,c) = pD . i ) ) ) or M1 = M2 )
assume that A13:
len M1 = len M
and A14:
width M1 = width M
and A15:
for
i,
j being
Nat st
[i,j] in Indices M holds
( (
j <> c implies
M1 * (
i,
j)
= M * (
i,
j) ) & (
j = c implies
M1 * (
i,
c)
= pD . i ) )
;
( not len M2 = len M or not width M2 = width M or ex i, j being Nat st
( [i,j] in Indices M & not ( ( j <> c implies M2 * (i,j) = M * (i,j) ) & ( j = c implies M2 * (i,c) = pD . i ) ) ) or M1 = M2 )
assume that
len M2 = len M
and
width M2 = width M
and A16:
for
i,
j being
Nat st
[i,j] in Indices M holds
( (
j <> c implies
M2 * (
i,
j)
= M * (
i,
j) ) & (
j = c implies
M2 * (
i,
c)
= pD . i ) )
;
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;
( [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 A17:
[i,j] in Indices M
by A13, A14, MATRIX_4:55;
reconsider I =
i,
J =
j as
Element of
NAT by ORDINAL1:def 12;
A18:
(
J = c implies
M1 * (
I,
c)
= pD . I )
by A15, A17;
A19:
(
J <> c implies
M2 * (
I,
J)
= M * (
I,
J) )
by A16, A17;
(
J <> c implies
M1 * (
I,
J)
= M * (
I,
J) )
by A15, A17;
hence
M1 * (
i,
j)
= M2 * (
i,
j)
by A16, A17, A18, A19;
verum
end;
hence
M1 = M2
by MATRIX_0:27;
verum
end;
thus
( not len pD = len M & M1 = M & M2 = M implies M1 = M2 )
; verum