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