reconsider N = n as Element of NAT by ORDINAL1:def 13;
deffunc H₁( Nat, Nat) -> Element of K = Cofactor M,$1,$2;
ex M being Matrix of N,N,K st
for i, j being Nat st [i,j] in Indices M holds
M * i,j = H₁(i,j) from MATRIX_1:sch 1();
hence 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 ; :: thesis: verum