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