reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
deffunc H₁( Nat, Nat) -> Element of the carrier of K = - (A * $1,$2);
consider M being Matrix of n1,K such that
A12: for i, j being Nat st [i,j] in Indices M holds
M * i,j = H₁(i,j) from MATRIX_1:sch 1();
Indices A = [:(Seg n),(Seg n):] by Th25;
then A13: Indices A = Indices M by Th25;
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 A12, A13; :: thesis: verum