deffunc H1( 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) = H1(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;
A3: now :: thesis: ( ( len M = 0 & width M1 = width M ) or ( len M > 0 & width M1 = width M ) )
per cases ( len M = 0 or len M > 0 ) ;
end;
end;
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
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