set X = {0};

deffunc H_{1}( 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_{1}(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

deffunc H

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

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