let IT be Function of A,BOOLEAN; :: thesis: ( IT = 'not' p iff for x being Element of A holds IT . x = 'not' (p . x) )
A2: dom IT = A by FUNCT_2:def 1;
hereby :: thesis: ( ( for x being Element of A holds IT . x = 'not' (p . x) ) implies IT = 'not' p )
assume A3: 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 A3, Def17; :: thesis: verum
end;
A4: dom p = A by FUNCT_2:def 1;
assume for x being Element of A holds IT . x = 'not' (p . x) ; :: thesis: IT = 'not' p
then for x being object st x in dom p holds
IT . x = 'not' (p . x) by A4;
hence IT = 'not' p by A2, A4, Def17; :: thesis: verum