let Y be non empty set ; :: thesis: for a1, a2, b1, b2, b3 being Element of Funcs 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)
let a1, a2, b1, b2, b3 be Element of Funcs Y,BOOLEAN ; :: thesis: (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) = (((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3)
(((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) = ((((a1 'or' (b1 '&' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) by BVFUNC_1:14
.= (((a1 'or' ((b1 '&' b2) '&' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) by BVFUNC_1:14
.= ((a1 'or' ((b1 '&' b2) '&' b3)) '&' ((a2 'or' b1) '&' (a2 'or' b2))) '&' (a2 'or' b3) by BVFUNC_1:7
.= (a1 'or' ((b1 '&' b2) '&' b3)) '&' (((a2 'or' b1) '&' (a2 'or' b2)) '&' (a2 'or' b3)) by BVFUNC_1:7
.= (a1 'or' ((b1 '&' b2) '&' b3)) '&' ((a2 'or' (b1 '&' b2)) '&' (a2 'or' b3)) by BVFUNC_1:14
.= (a1 'or' ((b1 '&' b2) '&' b3)) '&' (a2 'or' ((b1 '&' b2) '&' b3)) by BVFUNC_1:14
.= (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) by BVFUNC_1:14 ;
hence (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) = (((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) ; :: thesis: verum