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₁ being Matrix of n,m,D st b₁ = M )

proof

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 ) ) ) )
defpred S₁[ 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 ) );
reconsider V = n, U = m as Element of NAT by ORDINAL1:def 13;
A2: for i, j being Nat st [i,j] in [:(Seg V),(Seg U):] holds
for x1, x2 being Element of D st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2

proof

let i, j be Nat; :: thesis: ( [i,j] in [:(Seg V),(Seg U):] implies for x1, x2 being Element of D st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2 )
assume [i,j] in [:(Seg V),(Seg U):] ; :: thesis: for x1, x2 being Element of D st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2
let x1, x2 be Element of D; :: thesis: ( S₁[i,j,x1] & S₁[i,j,x2] implies x1 = x2 )
assume A3: ( S₁[i,j,x1] & S₁[i,j,x2] ) ; :: thesis: x1 = x2
reconsider i = i, j = j as Element of NAT by ORDINAL1:def 13;
( ( j <> c implies x1 = M * i,j ) & ( j = c implies x1 = pD . i ) & ( j <> c implies x2 = M * i,j ) & ( j = c implies x2 = pD . i ) ) by A3;
hence x1 = x2 ; :: thesis: verum

end;

A4: for i, j being Nat st [i,j] in [:(Seg V),(Seg U):] holds
ex x being Element of D st S₁[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 S₁[i,j,x] )
assume A5: [i,j] in [:(Seg V),(Seg U):] ; :: thesis: ex x being Element of D st S₁[i,j,x]

now

per cases ( j = c or j <> c ) ;

case A6: j = c ; :: thesis: ex x being Element of D st S₁[i,j,x]

len M = n by MATRIX_1:def 3;
then i in Seg (len pD) by A1, A5, ZFMISC_1:106;
then i in dom pD by FINSEQ_1:def 3;
then ( pD . i in rng pD & rng pD c= D ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then ( pD . i in D & S₁[i,j,pD . i] ) by A6;
hence ex x being Element of D st S₁[i,j,x] ; :: thesis: verum

end;

case j <> c ; :: thesis: ex x being Element of D st S₁[i,j,x]

then S₁[i,j,M * i,j] ;
hence ex x being Element of D st S₁[i,j,x] ; :: thesis: verum

end;

end;

end;

hence ex x being Element of D st S₁[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
S₁[i,j,M1 * i,j] from MATRIX_1:sch 2(A2, A4);
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

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: ( len M = len M1 & width M1 = width M )

then A9: ( len M = 0 & len M1 = 0 ) by MATRIX_1:def 3;
then ( width M1 = 0 & 0 = width M ) by MATRIX_1:def 4;
hence ( len M = len M1 & width M1 = width M ) by A9; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ( len M = len M1 & width M = width M1 )

then ( len M = n & len M1 = n & width M = m & width M1 = m ) by MATRIX_1:24;
hence ( len M = len M1 & width M = width M1 ) ; :: thesis: verum

end;

end;

end;

reconsider M' = M as Matrix of len M, width M,D by MATRIX_2:7;
( Indices M' = Indices M & Indices M' = Indices M1 ) by MATRIX_1:27;
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 b₁ being Matrix of n,m,D st b₁ = M ) ; :: thesis: verum