deffunc H₁( Nat, Nat) -> Element of K = Cofactor M,$1,$2;
reconsider N = n as Element of NAT by ORDINAL1:def 13;
consider M being Matrix of N,N,K such that
A1: for i, j being Nat st [i,j] in Indices M holds
M * i,j = H₁(i,j) from MATRIX_1:sch 1();
thus ex b₁ being Matrix of n,K st
for i, j being Nat st [i,j] in Indices b₁ holds
b₁ * i,j = Cofactor M,i,j by A1; :: thesis: verum