set n = len A;
deffunc H1( Nat, Nat) -> Element of the carrier of K = - (A * ($1,$2));
consider M being Matrix of len A, width A,K such that
A1:
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = H1(i,j)
from MATRIX_0:sch 1();
reconsider A1 = A as Matrix of len A, width A,K by MATRIX_0:51;
A2:
Indices A1 = [:(Seg (len A)),(Seg (width A)):]
by MATRIX_0:25;
reconsider M = M as Matrix of K ;
take
M
; ( len M = len A & width M = width A & ( for i, j being Nat st [i,j] in Indices A holds
M * (i,j) = - (A * (i,j)) ) )
thus
( len M = len A & width M = width A & ( for i, j being Nat st [i,j] in Indices A holds
M * (i,j) = - (A * (i,j)) ) )
by A1, A3; verum