deffunc H_{1}( Point of R^1, Point of R^1) -> Element of the carrier of K571() = R^1 ($1 * $2);

consider f being Function of [:R^1,R^1:],R^1 such that

A1: for s, t being Point of R^1 holds f . (s,t) = H_{1}(s,t)
from TOPALG_7:sch 1();

take f ; :: thesis: for x, y being Point of R^1 holds f . (x,y) = x * y

let x, y be Point of R^1; :: thesis: f . (x,y) = x * y

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

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

consider f being Function of [:R^1,R^1:],R^1 such that

A1: for s, t being Point of R^1 holds f . (s,t) = H

take f ; :: thesis: for x, y being Point of R^1 holds f . (x,y) = x * y

let x, y be Point of R^1; :: thesis: f . (x,y) = x * y

f . (x,y) = H

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