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