now

per cases ( width M > 0 or width M = 0 ) by NAT_1:3;

suppose A1: width M > 0 ; :: thesis: ex b₁ being Matrix of D st
( len b₁ = width M & ( for i, j being Nat holds
( [i,j] in Indices b₁ iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b₁ * i,j = M * j,i ) )

A2: Seg (len M) = dom M by FINSEQ_1:def 3;
deffunc H₁( Nat, Nat) -> Element of D = M * $2,$1;
consider M1 being Matrix of width M, len M,D such that
A3: for i, j being Nat st [i,j] in Indices M1 holds
M1 * i,j = H₁(i,j) from MATRIX_1:sch 1();
A4: Indices M1 = [:(Seg (width M)),(dom M):] by A1, A2, Th24;
reconsider M' = M1 as Matrix of D ;
thus ex b₁ being Matrix of D st
( len b₁ = width M & ( for i, j being Nat holds
( [i,j] in Indices b₁ iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b₁ * i,j = M * j,i ) ) :: thesis: verum

proof

take M' ; :: thesis: ( len M' = width M & ( for i, j being Nat holds
( [i,j] in Indices M' iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
M' * i,j = M * j,i ) )
thus len M' = width M by A1, Th24; :: thesis: ( ( for i, j being Nat holds
( [i,j] in Indices M' iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
M' * i,j = M * j,i ) )
thus for i, j being Nat holds
( [i,j] in Indices M' iff [j,i] in Indices M ) by A4, ZFMISC_1:107; :: thesis: for i, j being Nat st [j,i] in Indices M holds
M' * i,j = M * j,i
let i, j be Nat; :: thesis: ( [j,i] in Indices M implies M' * i,j = M * j,i )
assume [j,i] in Indices M ; :: thesis: M' * i,j = M * j,i
then [i,j] in Indices M' by A4, ZFMISC_1:107;
hence M' * i,j = M * j,i by A3; :: thesis: verum

end;

end;

suppose A5: width M = 0 ; :: thesis: ex b₁ being Matrix of D st
( len b₁ = width M & ( for i, j being Nat holds
( [i,j] in Indices b₁ iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b₁ * i,j = M * j,i ) )

reconsider M1 = {} as Matrix of D by Th13;
thus ex b₁ being Matrix of D st
( len b₁ = width M & ( for i, j being Nat holds
( [i,j] in Indices b₁ iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b₁ * i,j = M * j,i ) ) :: thesis: verum

proof

take M1 ; :: thesis: ( len M1 = width M & ( for i, j being Nat holds
( [i,j] in Indices M1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
M1 * i,j = M * j,i ) )
Indices M1 = [:{} ,(Seg (width M1)):] ;
hence ( len M1 = width M & ( for i, j being Nat holds
( [i,j] in Indices M1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
M1 * i,j = M * j,i ) ) by A5, FINSEQ_1:4, ZFMISC_1:113; :: thesis: verum

end;

end;

end;

end;

hence ex b₁ being Matrix of D st
( len b₁ = width M & ( for i, j being Nat holds
( [i,j] in Indices b₁ iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b₁ * i,j = M * j,i ) ) ; :: thesis: verum