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