deffunc H1( Nat, Nat) -> Element of COMPLEX = In ((((x . $1) * (M * ($1,$2))) * ((y . $2) *')),COMPLEX);
consider M1 being Matrix of len M, width M,COMPLEX such that
A3:
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = H1(i,j)
from MATRIX_0:sch 1();
take
M1
; ( len M1 = len x & width M1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) )
thus A4:
len M1 = len x
by A1, MATRIX_0:def 2; ( width M1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') ) )
A7:
dom M = dom M1
by A1, A4, FINSEQ_3:29;
let i, j be Nat; ( [i,j] in Indices M implies M1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *') )
assume
[i,j] in Indices M
; M1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *')
then
[i,j] in Indices M1
by A7, A5, A2;
then
M1 * (i,j) = H1(i,j)
by A3;
hence
M1 * (i,j) = ((x . i) * (M * (i,j))) * ((y . j) *')
; verum