thus ( len pD = width 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
( ( i <> l implies M1 * i,j = M * i,j ) & ( i = l implies M1 * l,j = pD . j ) ) ) ) ) :: thesis: ( not len pD = width M implies ex b₁ being Matrix of n,m,D st b₁ = M )

proof

reconsider M9 = M as Matrix of len M, width M,D by MATRIX_2:7;
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 13;
defpred S₁[ set , set , set ] means for i, j being Nat st i = $1 & j = $2 holds
( ( i <> l implies $3 = M * i,j ) & ( i = l implies $3 = pD . j ) );
assume A1: len pD = width 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
( ( i <> l implies M1 * i,j = M * i,j ) & ( i = l implies M1 * l,j = pD . j ) ) ) )
A2: for i, j being Nat st [i,j] in [:(Seg n1),(Seg m1):] holds
ex x being Element of D st S₁[i,j,x]

proof

let i, j be Nat; :: thesis: ( [i,j] in [:(Seg n1),(Seg m1):] implies ex x being Element of D st S₁[i,j,x] )
assume A3: [i,j] in [:(Seg n1),(Seg m1):] ; :: thesis: ex x being Element of D st S₁[i,j,x]

now

per cases ( i = l or i <> l ) ;

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

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

end;

case i <> l ; :: 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;

A7: for i, j being Nat st [i,j] in [:(Seg n1),(Seg m1):] 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 n1),(Seg m1):] 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 n1),(Seg m1):] ; :: 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 that
A8: S₁[i,j,x1] and
A9: S₁[i,j,x2] ; :: thesis: x1 = x2
A10: ( i = l implies x1 = pD . j ) by A8;
( i <> l implies x1 = M * i,j ) by A8;
hence x1 = x2 by A9, A10; :: thesis: verum

end;

consider M1 being Matrix of n1,m1,D such that
A11: for i, j being Nat st [i,j] in Indices M1 holds
S₁[i,j,M1 * i,j] from MATRIX_1:sch 2(A7, 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
( ( i <> l implies M1 * i,j = M * i,j ) & ( i = l implies M1 * l,j = pD . j ) ) ) )

A12: now

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

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

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

end;

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

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

end;

end;

end;

Indices M9 = 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
( ( i <> l implies M1 * i,j = M * i,j ) & ( i = l implies M1 * l,j = pD . j ) ) ) ) by A11, A12; :: thesis: verum

end;

thus ( not len pD = width M implies ex b₁ being Matrix of n,m,D st b₁ = M ) ; :: thesis: verum