let Y be non empty set ; :: thesis: for a, b being Function of Y,BOOLEAN holds 'not' (a 'xor' b) = a 'xor' ('not' b)
let a, b be Function of Y,BOOLEAN; :: thesis: 'not' (a 'xor' b) = a 'xor' ('not' b)
let x be Element of Y; :: according to FUNCT_2:def 8 :: thesis: K11(('not' (a 'xor' b)),x) = K11((a 'xor' ('not' b)),x)
('not' (a 'xor' b)) . x = ('not' ((('not' a) '&' b) 'or' (a '&' ('not' b)))) . x by BVFUNC_4:9
.= (('not' (('not' a) '&' b)) '&' ('not' (a '&' ('not' b)))) . x by BVFUNC_1:13
.= ((('not' ('not' a)) 'or' ('not' b)) '&' ('not' (a '&' ('not' b)))) . x by BVFUNC_1:14
.= ((a 'or' ('not' b)) '&' (('not' a) 'or' ('not' ('not' b)))) . x by BVFUNC_1:14
.= (((a 'or' ('not' b)) '&' ('not' a)) 'or' ((a 'or' ('not' b)) '&' b)) . x by BVFUNC_1:12
.= (((a '&' ('not' a)) 'or' (('not' b) '&' ('not' a))) 'or' ((a 'or' ('not' b)) '&' b)) . x by BVFUNC_1:12
.= (((O_el Y) 'or' (('not' b) '&' ('not' a))) 'or' ((a 'or' ('not' b)) '&' b)) . x by BVFUNC_4:5
.= ((('not' b) '&' ('not' a)) 'or' ((a 'or' ('not' b)) '&' b)) . x by BVFUNC_1:9
.= ((('not' b) '&' ('not' a)) 'or' ((a '&' b) 'or' (('not' b) '&' b))) . x by BVFUNC_1:12
.= ((('not' b) '&' ('not' a)) 'or' ((a '&' b) 'or' (O_el Y))) . x by BVFUNC_4:5
.= ((('not' a) '&' ('not' b)) 'or' (a '&' ('not' ('not' b)))) . x by BVFUNC_1:9
.= (a 'xor' ('not' b)) . x by BVFUNC_4:9 ;
hence K11(('not' (a 'xor' b)),x) = K11((a 'xor' ('not' b)),x) ; :: thesis: verum