let Y be non empty set ; :: thesis: for a, b, c, d being Function of Y,BOOLEAN holds a 'or' ((b '&' c) '&' d) = ((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d)
let a, b, c, d be Function of Y,BOOLEAN; :: thesis: a 'or' ((b '&' c) '&' d) = ((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d)
a 'or' ((b '&' c) '&' d) = (a 'or' (b '&' c)) '&' (a 'or' d) by BVFUNC_1:11
.= ((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d) by BVFUNC_1:11 ;
hence a 'or' ((b '&' c) '&' d) = ((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d) ; :: thesis: verum