set X = the carrier of B;

deffunc H_{1}( Element of B, Element of B, Element of B) -> Element of B = Ros ($1,$2,$3);

consider ff being Function of [: the carrier of B, the carrier of B, the carrier of B:], the carrier of B such that

A1: for x, y, z being Element of the carrier of B holds ff . (x,y,z) = H_{1}(x,y,z)
from MULTOP_1:sch 4();

reconsider ff = ff as TriOp of the carrier of B ;

take ff ; :: thesis: for a, b, c being Element of B holds ff . (a,b,c) = Ros (a,b,c)

thus for a, b, c being Element of B holds ff . (a,b,c) = Ros (a,b,c) by A1; :: thesis: verum

deffunc H

consider ff being Function of [: the carrier of B, the carrier of B, the carrier of B:], the carrier of B such that

A1: for x, y, z being Element of the carrier of B holds ff . (x,y,z) = H

reconsider ff = ff as TriOp of the carrier of B ;

take ff ; :: thesis: for a, b, c being Element of B holds ff . (a,b,c) = Ros (a,b,c)

thus for a, b, c being Element of B holds ff . (a,b,c) = Ros (a,b,c) by A1; :: thesis: verum