deffunc H1( Nat, Nat) -> Element of the carrier of K = a * (M * ($1,$2));
consider N being Matrix of len M, width M,K such that
A1:
for i, j being Nat st [i,j] in Indices N holds
N * (i,j) = H1(i,j)
from MATRIX_0:sch 1();
take
N
; ( len N = len M & width N = width M & ( for i, j being Nat st [i,j] in Indices M holds
N * (i,j) = a * (M * (i,j)) ) )
A2:
len N = len M
by MATRIX_0:def 2;
dom M = dom N
by A2, FINSEQ_3:29;
then
Indices N = [:(dom M),(Seg (width M)):]
by A3;
hence
( len N = len M & width N = width M & ( for i, j being Nat st [i,j] in Indices M holds
N * (i,j) = a * (M * (i,j)) ) )
by A1, A3, MATRIX_0:def 2; verum