deffunc H₁( Nat, Nat) -> Element of the carrier of K = - (A * ($1,$2));
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
consider M being Matrix of n1,K such that
A14: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = H₁(i,j) from MATRIX_0:sch 1();
Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A15: Indices A = Indices M by MATRIX_0:24;
reconsider M = M as Matrix of n,K ;
take M ; :: thesis: for i, j being Nat st [i,j] in Indices A holds
M * (i,j) = - (A * (i,j))
thus for i, j being Nat st [i,j] in Indices A holds
M * (i,j) = - (A * (i,j)) by A14, A15; :: thesis: verum