deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) -> Element of BOOLEAN = 'not' ((('not' $1) 'or' $2) 'or' $3);
thus
for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2
from FACIRC_1:sch 5(); verum