deffunc H₁( Nat, Nat) -> Element of the carrier of K = (Line A,$1) "*" (Col B,$2);
consider M being Matrix of len A, width B,K such that
A2: for i, j being Nat st [i,j] in Indices M holds
M * i,j = H₁(i,j) from MATRIX_1:sch 1();
take M ; :: thesis: ( len M = len A & width M = width B & ( for i, j being Nat st [i,j] in Indices M holds
M * i,j = (Line A,i) "*" (Col B,j) ) )

now

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

case len A > 0 ; :: thesis: ( len M = len A & width M = width B )

hence ( len M = len A & width M = width B ) by MATRIX_1:24; :: thesis: verum

end;

case A3: len A = 0 ; :: thesis: ( len M = len A & width M = width B )

then len B = 0 by A1, MATRIX_1:def 4;
then A4: width B = 0 by MATRIX_1:def 4;
len M = 0 by A3, MATRIX_1:26;
hence ( len M = len A & width M = width B ) by A3, A4, MATRIX_1:def 4; :: thesis: verum

end;

end;

end;

hence ( len M = len A & width M = width B & ( for i, j being Nat st [i,j] in Indices M holds
M * i,j = (Line A,i) "*" (Col B,j) ) ) by A2; :: thesis: verum