deffunc H1( 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) = H1(i,j)
from MATRIX_0:sch 1();
take
M
; 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))
verumproof
let i,
j be
Nat;
( 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 )
;
M * (i,j) = f . ((b1 /. i),(b2 /. j))
len b1 <> 0
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)
= H1(
i,
j)
by A20;
hence
M * (
i,
j)
= f . (
(b1 /. i),
(b2 /. j))
;
verum
end;