let IT be Element of Funcs (A,BOOLEAN); :: thesis: ( IT = p '&' q iff for x being Element of A holds IT . x = (p . x) '&' (q . x) )
A7: dom IT = A by FUNCT_2:def 1;

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

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

end;

A10: dom q = A by FUNCT_2:def 1;
A11: dom IT = A /\ A by FUNCT_2:def 1
.= (dom p) /\ (dom q) by A10, FUNCT_2:def 1 ;
assume for x being Element of A holds IT . x = (p . x) '&' (q . x) ; :: thesis: IT = p '&' q
then for x being set st x in dom IT holds
IT . x = (p . x) '&' (q . x) by A7;
hence IT = p '&' q by A11, Def19; :: thesis: verum