deffunc H_{1}( 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*> = H_{1}(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*> = H_{1}(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = H_{1}(x,y) ) holds

f1 = f2 ) ) from FACIRC_1:sch 3();

hence ( ex b_{1} being Function of (2 -tuples_on BOOLEAN),BOOLEAN st

for x, y being Element of BOOLEAN holds b_{1} . <*x,y*> = x '&' y & ( for b_{1}, b_{2} being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b_{1} . <*x,y*> = x '&' y ) & ( for x, y being Element of BOOLEAN holds b_{2} . <*x,y*> = x '&' y ) holds

b_{1} = b_{2} ) )
; :: thesis: verum

( ex f being Function of (2 -tuples_on BOOLEAN),BOOLEAN st

for x, y being Element of BOOLEAN holds f . <*x,y*> = H

f1 = f2 ) ) from FACIRC_1:sch 3();

hence ( ex b

for x, y being Element of BOOLEAN holds b

b