deffunc H₁( Nat, Nat) -> Element of COMPLEX = In ((((x . $1) * (M * ($1,$2))) * ((y . $2) *')),COMPLEX);
consider M1 being Matrix of len M, width M,COMPLEX such that
A3: 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:
thus A4: len M1 = len x by A1, MATRIX_0:def 2; :: thesis:

hereby :: thesis:

per cases ;

suppose A6: len M = 0 ; :: thesis:

then width M1 = 0 by A1, A4, MATRIX_0:def 3;
hence width M1 = len y by A2, A6, MATRIX_0:def 3; :: thesis:

end;

suppose len M > 0 ; :: thesis:

hence width M1 = len y by A2, MATRIX_0:23; :: thesis:

end;

end;

end;

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