now :: 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) ) )

per cases ( width M > 0 or width M = 0 ) ;

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

deffunc H₁( Nat, Nat) -> Element of D = M * ($2,$1);
consider M1 being Matrix of width M, len M,D such that
A2: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = H₁(i,j) from MATRIX_0:sch 1();
reconsider M9 = M1 as Matrix of D ;
Seg (len M) = dom M by FINSEQ_1:def 3;
then A3: Indices M1 = [:(Seg (width M)),(dom M):] by A1, Th23;
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 M9 ; :: thesis: ( len M9 = width M & ( for i, j being Nat holds
( [i,j] in Indices M9 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
M9 * (i,j) = M * (j,i) ) )
thus len M9 = width M by A1, Th23; :: thesis: ( ( for i, j being Nat holds
( [i,j] in Indices M9 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
M9 * (i,j) = M * (j,i) ) )
thus for i, j being Nat holds
( [i,j] in Indices M9 iff [j,i] in Indices M ) by A3, ZFMISC_1:88; :: thesis: for i, j being Nat st [j,i] in Indices M holds
M9 * (i,j) = M * (j,i)
let i, j be Nat; :: thesis: ( [j,i] in Indices M implies M9 * (i,j) = M * (j,i) )
assume [j,i] in Indices M ; :: thesis: M9 * (i,j) = M * (j,i)
then [i,j] in Indices M9 by A3, ZFMISC_1:88;
hence M9 * (i,j) = M * (j,i) by A2; :: thesis: verum

end;

end;

suppose A4: 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) ) )
A5: Indices M1 = [:{},(Seg (width M1)):] ;
Seg (width M) = {} by A4;
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, ZFMISC_1:90; :: 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