set X = the carrier of B;
deffunc H₁( 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₁(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