deffunc H₁( Element of BOOLEAN ) -> Element of BOOLEAN = 'not' $1;
thus ex t being Function of (1 -tuples_on BOOLEAN),BOOLEAN st
for x being Element of BOOLEAN holds t . <*x*> = H₁(x) from GFACIRC1:sch 1(); :: thesis: verum