deffunc H₁( Nat, Nat) -> Element of REAL = In ((((x . $1) * (M * ($1,$2))) * (y . $2)),REAL);
consider M1 being Matrix of len M, width M,REAL such that
A3: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = H₁(i,j) from MATRIX_0:sch 1();
take M1 ; :: thesis: ( 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; :: thesis: ( 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) ) )

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

per cases ( len M = 0 or len M > 0 ) ;

case A6: len M = 0 ; :: thesis: width M1 = len y

then width M1 = 0 by A1, A4, MATRIX_0:def 3;
hence width M1 = len y by A2, A6, MATRIX_0:def 3; :: thesis: verum

end;

case len M > 0 ; :: thesis: width M1 = len y

hence width M1 = len y by A2, MATRIX_0:23; :: thesis: verum

end;

end;

end;

A7: Indices M = [:(dom M),(Seg (width M)):] by MATRIX_0:def 4;
dom M = dom M1 by A1, A4, FINSEQ_3:29;
then A8: Indices M1 = [:(dom M),(Seg (width M)):] by A2, A5, MATRIX_0:def 4;
thus width M1 = len y by A5; :: thesis: for i, j being Nat st [i,j] in Indices M holds
M1 * (i,j) = ((x . i) * (M * (i,j))) * (y . j)
let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M1 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) )
assume [i,j] in Indices M ; :: thesis: M1 * (i,j) = ((x . i) * (M * (i,j))) * (y . j)
hence M1 * (i,j) = H₁(i,j) by A3, A7, A8
.= ((x . i) * (M * (i,j))) * (y . j) ;
:: thesis: verum