deffunc H₁( Nat, Nat) -> Element of the carrier of K = (M * ($1,$2)) * a;
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) = H₁(i,j) from MATRIX_0:sch 1();
take N ; :: thesis: ( len N = len M & width N = width M & ( for i, j being Nat st [i,j] in Indices M holds
N * (i,j) = (M * (i,j)) * a ) )
A2: len N = len M by MATRIX_0:def 2;

A3: now :: thesis: ( ( len M = 0 & width N = width M ) or ( len M > 0 & width N = width M ) )

per cases ( len M = 0 or len M > 0 ) ;

case A4: len M = 0 ; :: thesis: width N = width M

then width N = 0 by A2, MATRIX_0:def 3;
hence width N = width M by A4, MATRIX_0:def 3; :: thesis: verum

end;

case len M > 0 ; :: thesis: width N = width M

hence width N = width M by MATRIX_0:23; :: thesis: verum

end;

end;

end;

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) = (M * (i,j)) * a ) ) by A1, A3, MATRIX_0:def 2; :: thesis: verum