deffunc H₁( Nat, Nat) -> Element of the carrier of INT.Ring = In ((f . ((b1 /. $1),(b2 /. $2))), the carrier of INT.Ring);
consider M being Matrix of len b1, len b2,INT.Ring 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();
take M ; :: thesis: for i, j being Nat st i in dom b1 & j in dom b2 holds
M * (i,j) = f . ((b1 /. i),(b2 /. j))
thus for i, j being Nat st i in dom b1 & j in dom b2 holds
M * (i,j) = f . ((b1 /. i),(b2 /. j)) :: thesis: verum

proof

let i, j be Nat; :: thesis: ( i in dom b1 & j in dom b2 implies M * (i,j) = f . ((b1 /. i),(b2 /. j)) )
assume A21: ( i in dom b1 & j in dom b2 ) ; :: thesis: M * (i,j) = f . ((b1 /. i),(b2 /. j))
len b1 <> 0

proof

assume len b1 = 0 ; :: thesis: contradiction
then Seg (len b1) = {} ;
hence contradiction by A21, FINSEQ_1:def 3; :: thesis: verum

end;

then Indices M = [:(Seg (len b1)),(Seg (len b2)):] by MATRIX_0:23
.= [:(dom b1),(Seg (len b2)):] by FINSEQ_1:def 3
.= [:(dom b1),(dom b2):] by FINSEQ_1:def 3 ;
then [i,j] in Indices M by A21, ZFMISC_1:87;
then M * (i,j) = H₁(i,j) by A20;
hence M * (i,j) = f . ((b1 /. i),(b2 /. j)) ; :: thesis: verum

end;