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

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

assume A10: IT = p 'eqv' q ; :: thesis: for x being Element of A holds IT . x = 'not' ((p . x) 'xor' (q . x))
let x be Element of A; :: thesis: IT . x = 'not' ((p . x) 'xor' (q . x))
A11: dom p = A by FUNCT_2:def 1;
dom q = A by FUNCT_2:def 1;
then dom (p 'eqv' q) = A /\ A by A11, Def10
.= A ;
hence IT . x = 'not' ((p . x) 'xor' (q . x)) by A10, Def10; :: thesis: verum

end;

assume A12: for x being Element of A holds IT . x = 'not' ((p . x) 'xor' (q . x)) ; :: thesis: IT = p 'eqv' q
A13: dom q = A by FUNCT_2:def 1;
A14: dom IT = A /\ A by FUNCT_2:def 1
.= (dom p) /\ (dom q) by A13, FUNCT_2:def 1 ;
for x being set st x in dom IT holds
IT . x = (p . x) <=> (q . x)

proof

let x be set ; :: thesis: ( x in dom IT implies IT . x = (p . x) <=> (q . x) )
assume x in dom IT ; :: thesis: IT . x = (p . x) <=> (q . x)
then reconsider x = x as Element of A by FUNCT_2:def 1;
IT . x = 'not' ((p . x) 'xor' (q . x)) by A12;
hence IT . x = (p . x) <=> (q . x) ; :: thesis: verum

end;

hence IT = p 'eqv' q by A14, Def10; :: thesis: verum