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_0: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 :: thesis: ( ( len A > 0 & len M = len A & width M = width B ) or ( len A = 0 & len M = len A & width M = width B ) )

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_0:23; :: thesis: verum

end;

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

then len B = 0 by A1, MATRIX_0:def 3;
then A4: width B = 0 by MATRIX_0:def 3;
len M = 0 by A3, MATRIX_0:25;
hence ( len M = len A & width M = width B ) by A3, A4, MATRIX_0:def 3; :: 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