deffunc H_{1}( Nat, Nat) -> Element of REAL = In (|.(M * ($1,$2)).|,REAL);

consider M1 being Matrix of len M, width M,REAL such that

A1: for i, j being Nat st [i,j] in Indices M1 holds

M1 * (i,j) = H_{1}(i,j)
from MATRIX_0:sch 1();

take M1 ; :: thesis: ( 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)).| ) )

A2: len M1 = len M by MATRIX_0:def 2;

M1 * (i,j) = |.(M * (i,j)).|

let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M1 * (i,j) = |.(M * (i,j)).| )

assume A5: [i,j] in Indices M ; :: thesis: M1 * (i,j) = |.(M * (i,j)).|

dom M = dom M1 by A2, FINSEQ_3:29;

hence M1 * (i,j) = In (|.(M * (i,j)).|,REAL) by A1, A3, A5

.= |.(M * (i,j)).| ;

:: thesis: verum

consider M1 being Matrix of len M, width M,REAL such that

A1: for i, j being Nat st [i,j] in Indices M1 holds

M1 * (i,j) = H

take M1 ; :: thesis: ( 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)).| ) )

A2: len M1 = len M by MATRIX_0:def 2;

A3: now :: thesis: ( ( len M = 0 & width M1 = width M ) or ( len M > 0 & width M1 = width M ) )

thus
( len M1 = len M & width M1 = width M )
by A3, A2; :: thesis: for i, j being Nat st [i,j] in Indices M holds end;

M1 * (i,j) = |.(M * (i,j)).|

let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M1 * (i,j) = |.(M * (i,j)).| )

assume A5: [i,j] in Indices M ; :: thesis: M1 * (i,j) = |.(M * (i,j)).|

dom M = dom M1 by A2, FINSEQ_3:29;

hence M1 * (i,j) = In (|.(M * (i,j)).|,REAL) by A1, A3, A5

.= |.(M * (i,j)).| ;

:: thesis: verum