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;
A3: now :: thesis: ( ( len A > 0 & len M = len A & width M = width A & Indices A = Indices M ) or ( len A = 0 & len M = len A & width M = width A & Indices A = Indices M ) )
per cases ( len A > 0 or len A = 0 ) ;
case len A > 0 ; :: thesis: ( len M = len A & width M = width A & Indices A = Indices M )
hence ( len M = len A & width M = width A & Indices A = Indices M ) by A2, MATRIX_0:23; :: thesis: verum
end;
end;
end;
reconsider M = M as Matrix of K ;
take M ; :: thesis: ( 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; :: thesis: verum