let M1, M2 be Matrix of n,m,D; :: thesis: ( ( 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 ) :: thesis: ( not len pD = len M & M1 = M & M2 = M implies M1 = M2 )

( ( 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 ) :: thesis: ( not len pD = len M & M1 = M & M2 = M implies M1 = M2 )

proof

thus
( not len pD = len M & M1 = M & M2 = M implies M1 = M2 )
; :: thesis: verum
assume
len pD = len 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 ( ( 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 ) ) ; :: 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 ( ( 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 ) ) ; :: thesis: M1 = M2

for i, j being Nat st [i,j] in Indices M1 holds

M1 * (i,j) = M2 * (i,j)

end;( [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 ) ) ; :: 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 ( ( 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 ) ) ; :: thesis: M1 = M2

for i, j being Nat st [i,j] in Indices M1 holds

M1 * (i,j) = M2 * (i,j)

proof

hence
M1 = M2
by MATRIX_0:27; :: thesis: verum
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 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; :: thesis: verum

end;assume [i,j] in Indices M1 ; :: thesis: 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; :: thesis: verum