let Y be non empty set ; :: thesis: for a, b, c, d being Element of Funcs (Y,BOOLEAN) holds a 'or' ((b '&' c) '&' d) = ((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d)
let a, b, c, d be Element of Funcs (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