deffunc H₁( Element of REAL n, Element of REAL n) -> Element of REAL = Sum (mlt ($1,$2));
ex f being Function of [:(REAL n),(REAL n):],REAL st
for x, y being Element of REAL n holds f . (x,y) = H₁(x,y) from BINOP_1:sch 4();
hence ex b₁ being Function of [:(REAL n),(REAL n):],REAL st
for x, y being Element of REAL n holds b₁ . (x,y) = Sum (mlt (x,y)) ; :: thesis: verum