thus
( len pD = len M implies ex M1 being Matrix of n,m,D st

( 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 ) ) ) ) ) :: thesis: ( not len pD = len M implies ex b_{1} being Matrix of n,m,D st b_{1} = M )_{1} being Matrix of n,m,D st b_{1} = M )
; :: thesis: verum

( 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 ) ) ) ) ) :: thesis: ( not len pD = len M implies ex b

proof

thus
( not len pD = len M implies ex b
reconsider M9 = M as Matrix of len M, width M,D by MATRIX_0:51;

reconsider V = n, U = m as Element of NAT by ORDINAL1:def 12;

defpred S_{1}[ set , set , set ] means for i, j being Nat st i = $1 & j = $2 holds

( ( j <> c implies $3 = M * (i,j) ) & ( j = c implies $3 = pD . i ) );

assume A1: len pD = len M ; :: thesis: ex M1 being Matrix of n,m,D st

( 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 ) ) ) )

A2: for i, j being Nat st [i,j] in [:(Seg V),(Seg U):] holds

ex x being Element of D st S_{1}[i,j,x]

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

S_{1}[i,j,M1 * (i,j)]
from MATRIX_0:sch 2(A2);

reconsider M1 = M1 as Matrix of n,m,D ;

take M1 ; :: thesis: ( 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 ) ) ) )

hence ( 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 ) ) ) ) by A7, A8; :: thesis: verum

end;reconsider V = n, U = m as Element of NAT by ORDINAL1:def 12;

defpred S

( ( j <> c implies $3 = M * (i,j) ) & ( j = c implies $3 = pD . i ) );

assume A1: len pD = len M ; :: thesis: ex M1 being Matrix of n,m,D st

( 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 ) ) ) )

A2: for i, j being Nat st [i,j] in [:(Seg V),(Seg U):] holds

ex x being Element of D st S

proof

consider M1 being Matrix of V,U,D such that
let i, j be Nat; :: thesis: ( [i,j] in [:(Seg V),(Seg U):] implies ex x being Element of D st S_{1}[i,j,x] )

assume A3: [i,j] in [:(Seg V),(Seg U):] ; :: thesis: ex x being Element of D st S_{1}[i,j,x]

_{1}[i,j,x]
; :: thesis: verum

end;assume A3: [i,j] in [:(Seg V),(Seg U):] ; :: thesis: ex x being Element of D st S

now :: thesis: ( ( j = c & ex x being Element of D st S_{1}[i,j,x] ) or ( j <> c & ex x being Element of D st S_{1}[i,j,x] ) )end;

hence
ex x being Element of D st Sper cases
( j = c or j <> c )
;

end;

case A4:
j = c
; :: thesis: ex x being Element of D st S_{1}[i,j,x]

A5:
rng pD c= D
by FINSEQ_1:def 4;

len M = n by MATRIX_0:def 2;

then i in Seg (len pD) by A1, A3, ZFMISC_1:87;

then i in dom pD by FINSEQ_1:def 3;

then A6: pD . i in rng pD by FUNCT_1:def 3;

S_{1}[i,j,pD . i]
by A4;

hence ex x being Element of D st S_{1}[i,j,x]
by A6, A5; :: thesis: verum

end;len M = n by MATRIX_0:def 2;

then i in Seg (len pD) by A1, A3, ZFMISC_1:87;

then i in dom pD by FINSEQ_1:def 3;

then A6: pD . i in rng pD by FUNCT_1:def 3;

S

hence ex x being Element of D st S

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

S

reconsider M1 = M1 as Matrix of n,m,D ;

take M1 ; :: thesis: ( 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 ) ) ) )

A8: now :: thesis: ( len M = len M1 & width M1 = width M )end;

Indices M9 = Indices M1
by MATRIX_0:26;per cases
( n = 0 or n > 0 )
;

end;

hence ( 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 ) ) ) ) by A7, A8; :: thesis: verum