deffunc H₁( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) -> Element of BOOLEAN = ($1 'or' $2) 'or' $3;
( ex f being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds f . <*x,y,z*> = H₁(x,y,z) & ( for f1, f2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds f1 . <*x,y,z*> = H₁(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = H₁(x,y,z) ) holds
f1 = f2 ) ) from FACIRC_1:sch 6();
hence ( ex b₁ being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b₁ . <*x,y,z*> = (x 'or' y) 'or' z & ( for b₁, b₂ being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b₁ . <*x,y,z*> = (x 'or' y) 'or' z ) & ( for x, y, z being Element of BOOLEAN holds b₂ . <*x,y,z*> = (x 'or' y) 'or' z ) holds
b₁ = b₂ ) ) ; :: thesis: verum