reconsider N = n as Element of NAT by ORDINAL1:def 12;

deffunc H_{1}( 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_{1}(i,j)
from MATRIX_0:sch 1();

hence ex b_{1} being Matrix of n,K st

for i, j being Nat st [i,j] in Indices b_{1} holds

b_{1} * (i,j) = Cofactor (M,i,j)
; :: thesis: verum

deffunc H

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

hence ex b

for i, j being Nat st [i,j] in Indices b

b