theorem :: BVFUNC_6:79

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (a '&' b) 'or' (a '&' ('not' b))