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
A1: (O_el Y) 'nand' a = 'not' ((O_el Y) '&' a) by Th1;
(O_el Y) '&' a = O_el Y by BVFUNC_1:8;
hence (O_el Y) 'nand' a = I_el Y by A1, BVFUNC_1:5; :: thesis: verum