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