deffunc H_{1}( Element of REAL n, Element of REAL n) -> Element of REAL = In ((Sum (mlt ($1,$2))),REAL);

consider f being Function of [:(REAL n),(REAL n):],REAL such that

A1: for x, y being Element of REAL n holds f . (x,y) = H_{1}(x,y)
from BINOP_1:sch 4();

take f ; :: thesis: for x, y being Element of REAL n holds f . (x,y) = Sum (mlt (x,y))

let x, y be Element of REAL n; :: thesis: f . (x,y) = Sum (mlt (x,y))

f . (x,y) = H_{1}(x,y)
by A1;

hence f . (x,y) = Sum (mlt (x,y)) ; :: thesis: verum

consider f being Function of [:(REAL n),(REAL n):],REAL such that

A1: for x, y being Element of REAL n holds f . (x,y) = H

take f ; :: thesis: for x, y being Element of REAL n holds f . (x,y) = Sum (mlt (x,y))

let x, y be Element of REAL n; :: thesis: f . (x,y) = Sum (mlt (x,y))

f . (x,y) = H

hence f . (x,y) = Sum (mlt (x,y)) ; :: thesis: verum