set X = {0};
deffunc H₁( Element of {0}, Element of {0}, Element of {0}) -> Element of {0} = In (0,{0});
consider ff being Function of [:{0},{0},{0}:],{0} such that
A1: for x, y, z being Element of {0} holds ff . (x,y,z) = H₁(x,y,z) from MULTOP_1:sch 4();
reconsider ff = ff as TriOp of {0} ;
take ff ; :: thesis: ff . (0,0,0) = 0
0 in {0} by TARSKI:def 1;
then ff . (0,0,0) = In (0,{0}) by A1
.= 0 by TARSKI:def 1 ;
hence ff . (0,0,0) = 0 ; :: thesis: verum