deffunc H_{1}( Nat, Nat) -> Element of the carrier of K = (A * ($1,$2)) + (B * ($1,$2));

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

consider M being Matrix of n1,K such that

A20: for i, j being Nat st [i,j] in Indices M holds

M * (i,j) = H_{1}(i,j)
from MATRIX_0:sch 1();

Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24;

then A21: Indices A = Indices M by MATRIX_0:24;

reconsider M = M as Matrix of n,K ;

take M ; :: thesis: for i, j being Nat st [i,j] in Indices A holds

M * (i,j) = (A * (i,j)) + (B * (i,j))

thus for i, j being Nat st [i,j] in Indices A holds

M * (i,j) = (A * (i,j)) + (B * (i,j)) by A20, A21; :: thesis: verum

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

consider M being Matrix of n1,K such that

A20: for i, j being Nat st [i,j] in Indices M holds

M * (i,j) = H

Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24;

then A21: Indices A = Indices M by MATRIX_0:24;

reconsider M = M as Matrix of n,K ;

take M ; :: thesis: for i, j being Nat st [i,j] in Indices A holds

M * (i,j) = (A * (i,j)) + (B * (i,j))

thus for i, j being Nat st [i,j] in Indices A holds

M * (i,j) = (A * (i,j)) + (B * (i,j)) by A20, A21; :: thesis: verum