let Y be non empty set ; :: thesis: for a being Element of Funcs Y,BOOLEAN holds (O_el Y) 'nand' a = I_el Y
let a be Element of Funcs Y,BOOLEAN ; :: thesis: (O_el Y) 'nand' a = I_el Y
( (O_el Y) 'nand' a = 'not' ((O_el Y) '&' a) & (O_el Y) '&' a = O_el Y ) by Th1, BVFUNC_1:8;
hence (O_el Y) 'nand' a = I_el Y by BVFUNC_1:5; :: thesis: verum