deffunc H_{1}( Element of {0,1,2}, Element of {0,1,2}) -> Element of {0,1,2} = $1 * $2;

ex o being BinOp of {0,1,2} st

for a, b being Element of {0,1,2} holds o . (a,b) = H_{1}(a,b)
from BINOP_1:sch 4();

hence ex b_{1} being BinOp of {0,1,2} st

for a, b being Element of {0,1,2} holds b_{1} . (a,b) = a * b
; :: thesis: verum

ex o being BinOp of {0,1,2} st

for a, b being Element of {0,1,2} holds o . (a,b) = H

hence ex b

for a, b being Element of {0,1,2} holds b