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) )

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 p = A by FUNCT_2:def 1;
dom q = 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;

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