deffunc H₁( 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₁(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