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