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