reconsider N = n as Element of NAT by ORDINAL1:def 12;
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_0: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