let Y be non empty set ; for a, b, c being Function of Y,BOOLEAN holds a '&' (b 'xor' c) = (a '&' b) 'xor' (a '&' c)
let a, b, c be Function of Y,BOOLEAN; a '&' (b 'xor' c) = (a '&' b) 'xor' (a '&' c)
A1: (a '&' b) 'xor' (a '&' c) =
(('not' (a '&' b)) '&' (a '&' c)) 'or' ((a '&' b) '&' ('not' (a '&' c)))
by BVFUNC_4:9
.=
((('not' a) 'or' ('not' b)) '&' (a '&' c)) 'or' ((a '&' b) '&' ('not' (a '&' c)))
by BVFUNC_1:14
.=
((a '&' c) '&' (('not' a) 'or' ('not' b))) 'or' ((a '&' b) '&' (('not' a) 'or' ('not' c)))
by BVFUNC_1:14
.=
(((a '&' c) '&' ('not' a)) 'or' ((a '&' c) '&' ('not' b))) 'or' ((a '&' b) '&' (('not' a) 'or' ('not' c)))
by BVFUNC_1:12
.=
(((a '&' c) '&' ('not' a)) 'or' ((a '&' c) '&' ('not' b))) 'or' (((a '&' b) '&' ('not' a)) 'or' ((a '&' b) '&' ('not' c)))
by BVFUNC_1:12
.=
((a '&' c) '&' ('not' a)) 'or' (((a '&' c) '&' ('not' b)) 'or' (((a '&' b) '&' ('not' c)) 'or' ((a '&' b) '&' ('not' a))))
by BVFUNC_1:8
.=
((a '&' c) '&' ('not' a)) 'or' ((((a '&' c) '&' ('not' b)) 'or' ((a '&' b) '&' ('not' c))) 'or' ((a '&' b) '&' ('not' a)))
by BVFUNC_1:8
.=
(((a '&' c) '&' ('not' a)) 'or' ((a '&' b) '&' ('not' a))) 'or' (((a '&' c) '&' ('not' b)) 'or' ((a '&' b) '&' ('not' c)))
by BVFUNC_1:8
;
A2: ((c '&' a) '&' ('not' a)) 'or' ((b '&' a) '&' ('not' a)) =
(c '&' (a '&' ('not' a))) 'or' ((b '&' a) '&' ('not' a))
by BVFUNC_1:4
.=
(c '&' (a '&' ('not' a))) 'or' (b '&' (a '&' ('not' a)))
by BVFUNC_1:4
.=
(c '&' (O_el Y)) 'or' (b '&' (a '&' ('not' a)))
by BVFUNC_4:5
.=
(c '&' (O_el Y)) 'or' (b '&' (O_el Y))
by BVFUNC_4:5
.=
(O_el Y) 'or' (b '&' (O_el Y))
by BVFUNC_1:5
.=
(O_el Y) 'or' (O_el Y)
by BVFUNC_1:5
.=
O_el Y
;
a '&' (b 'xor' c) =
a '&' ((('not' b) '&' c) 'or' (b '&' ('not' c)))
by BVFUNC_4:9
.=
(a '&' (('not' b) '&' c)) 'or' (a '&' (b '&' ('not' c)))
by BVFUNC_1:12
.=
((a '&' c) '&' ('not' b)) 'or' (a '&' (b '&' ('not' c)))
by BVFUNC_1:4
.=
((a '&' c) '&' ('not' b)) 'or' ((a '&' b) '&' ('not' c))
by BVFUNC_1:4
;
hence
a '&' (b 'xor' c) = (a '&' b) 'xor' (a '&' c)
by A1, A2, BVFUNC_1:9; verum