theorem :: BVFUNC_6:150
for Y being non empty set
for a1, a2, b1, b2, b3 being Function of Y,BOOLEAN holds (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) = (((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3)