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