let IT be Element of Funcs A,BOOLEAN ; :: thesis: ( IT = p 'nand' q iff for x being Element of A holds IT . x = (p . x) 'nand' (q . x) )

hereby :: thesis: ( ( for x being Element of A holds IT . x = (p . x) 'nand' (q . x) ) implies IT = p 'nand' q )

assume A3: IT = p 'nand' q ; :: thesis: for x being Element of A holds IT . x = (p . x) 'nand' (q . x)
let x be Element of A; :: thesis: IT . x = (p . x) 'nand' (q . x)
A4: dom p = A by FUNCT_2:def 1;
dom q = A by FUNCT_2:def 1;
then dom (p 'nand' q) = A /\ A by A4, Def1
.= A ;
hence IT . x = (p . x) 'nand' (q . x) by A3, Def1; :: thesis: verum

end;

assume A5: for x being Element of A holds IT . x = (p . x) 'nand' (q . x) ; :: thesis: IT = p 'nand' q
A6: dom IT = A by FUNCT_2:def 1;
A7: dom q = A by FUNCT_2:def 1;
A8: dom IT = A /\ A by FUNCT_2:def 1
.= (dom p) /\ (dom q) by A7, FUNCT_2:def 1 ;
for x being set st x in dom IT holds
IT . x = (p . x) 'nand' (q . x) by A5, A6;
hence IT = p 'nand' q by A8, Def1; :: thesis: verum