set n = len A;
reconsider A1 = A as Matrix of len A, width A,K by MATRIX_2:7;
deffunc H₁( Nat, Nat) -> Element of the carrier of K = (A * $1,$2) + (B * $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 = H₁(i,j) from MATRIX_1:sch 1();
A2: Indices A1 = [:(Seg (len A)),(Seg (width A)):] by MATRIX_1:26;

A3: now

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_1:24; :: thesis: verum

end;

case A4: len A = 0 ; :: thesis: ( len M = len A & width M = width A & Indices A = Indices M )

then len M = 0 by MATRIX_1:def 3;
then A5: width M = 0 by MATRIX_1:def 4;
width A = 0 by A4, MATRIX_1:def 4;
hence ( len M = len A & width M = width A & Indices A = Indices M ) by A2, A5, MATRIX_1:26; :: 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) + (B * 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) + (B * i,j) ) ) by A1, A3; :: thesis: verum