deffunc H1( Element of BOOLEAN , Element of BOOLEAN ) -> Element of BOOLEAN = $1 '&' $2;
( ex f being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds f . <*x,y*> = H1(x,y) & ( for f1, f2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds f1 . <*x,y*> = H1(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = H1(x,y) ) holds
f1 = f2 ) )
from FACIRC_1:sch 3();
hence
( ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y & ( for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x '&' y ) holds
b1 = b2 ) )
; verum