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

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

assume A2: IT = 'not' p ; :: thesis: for x being Element of A holds IT . x = 'not' (p . x)
let x be Element of A; :: thesis: IT . x = 'not' (p . x)
x in A ;
then x in dom p by FUNCT_2:def 1;
hence IT . x = 'not' (p . x) by A2, Def18; :: thesis: verum

end;

assume A3: for x being Element of A holds IT . x = 'not' (p . x) ; :: thesis: IT = 'not' p
A4: dom IT = A by FUNCT_2:def 1;
A5: dom p = A by FUNCT_2:def 1;
then for x being set st x in dom p holds
IT . x = 'not' (p . x) by A3;
hence IT = 'not' p by A4, A5, Def18; :: thesis: verum