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 b1 being Matrix of n,m,D st b1 = M )
proof
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 S1[ 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 S1[i,j,x]
proof
let i, j be Nat; :: thesis: ( [i,j] in [:(Seg V),(Seg U):] implies ex x being Element of D st S1[i,j,x] )
assume A3: [i,j] in [:(Seg V),(Seg U):] ; :: thesis: ex x being Element of D st S1[i,j,x]
now :: thesis: ( ( j = c & ex x being Element of D st S1[i,j,x] ) or ( j <> c & ex x being Element of D st S1[i,j,x] ) )
per cases ( j = c or j <> c ) ;
case A4: j = c ; :: thesis: ex x being Element of D st S1[i,j,x]
end;
case j <> c ; :: thesis: ex x being Element of D st S1[i,j,x]
then S1[i,j,M * (i,j)] ;
hence ex x being Element of D st S1[i,j,x] ; :: thesis: verum
end;
end;
end;
hence ex x being Element of D st S1[i,j,x] ; :: thesis: verum
end;
consider M1 being Matrix of V,U,D such that
A7: for i, j being Nat st [i,j] in Indices M1 holds
S1[i,j,M1 * (i,j)] from 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 )
per cases ( n = 0 or n > 0 ) ;
suppose A9: n = 0 ; :: thesis: ( len M = len M1 & width M1 = width M )
then len M1 = 0 by MATRIX_0:def 2;
then A10: width M1 = 0 by MATRIX_0:def 3;
len M = 0 by ;
hence ( len M = len M1 & width M1 = width M ) by ; :: thesis: verum
end;
suppose A11: n > 0 ; :: thesis: ( len M = len M1 & width M = width M1 )
then A12: width M = m by MATRIX_0:23;
len M = n by ;
hence ( len M = len M1 & width M = width M1 ) by ; :: thesis: verum
end;
end;
end;
Indices M9 = Indices M1 by MATRIX_0:26;
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;
thus ( not len pD = len M implies ex b1 being Matrix of n,m,D st b1 = M ) ; :: thesis: verum