deffunc H₁( Nat, Nat) -> Element of COMPLEX = In (((M * ($1,$2)) *'),COMPLEX);
consider M1 being Matrix of len M, width M,COMPLEX such that
A1: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = H₁(i,j) from MATRIX_0: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) = (M * (i,j)) *' ) )
thus A2: len M1 = len M by MATRIX_0:def 2; :: thesis: ( width M1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = (M * (i,j)) *' ) )

hereby :: thesis: for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = (M * (i,j)) *'

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

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

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

end;

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

hence width M1 = width M by MATRIX_0:23; :: thesis: verum

end;

end;

end;

A5: dom M = dom M1 by A2, FINSEQ_3:29;
let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M1 * (i,j) = (M * (i,j)) *' )
assume [i,j] in Indices M ; :: thesis: M1 * (i,j) = (M * (i,j)) *'
then [i,j] in Indices M1 by A3, A5;
then M1 * (i,j) = H₁(i,j) by A1;
hence M1 * (i,j) = (M * (i,j)) *' ; :: thesis: verum