deffunc H₁( Nat, Nat) -> Element of REAL = abs (M * $1,$2);
consider M1 being Matrix of len M, width M, REAL such that
A1: for i, j being Nat st [i,j] in Indices M1 holds
M1 * i,j = H₁(i,j) from MATRIX_1:sch 1();
take M1 ; :: thesis: ( len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
M1 * i,j = abs (M * i,j) ) )
A2: len M1 = len M by MATRIX_1:def 3;

A3: now

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

case A4: len M = 0 ; :: thesis: width M1 = width M

then width M1 = 0 by A2, MATRIX_1:def 4;
hence width M1 = width M by A4, MATRIX_1:def 4; :: thesis: verum

end;

case len M > 0 ; :: thesis: width M1 = width M

hence width M1 = width M by MATRIX_1:24; :: thesis: verum

end;

end;

end;

dom M = dom M1 by A2, FINSEQ_3:31;
hence ( len M1 = len M & width M1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
M1 * i,j = abs (M * i,j) ) ) by A1, A3, MATRIX_1:def 3; :: thesis: verum