deffunc H₁( Point of R^1, Point of R^1) -> Element of the carrier of K574() = 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₁(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₁(x,y) by A1;
hence f . (x,y) = x * y ; :: thesis: verum