let p, q be boolean-valued Function; :: thesis: for x being set st x in (dom p) /\ (dom q) holds
( (p '&' q) . x = TRUE iff ( p . x = TRUE & q . x = TRUE ) )
let x be set ; :: thesis: ( x in (dom p) /\ (dom q) implies ( (p '&' q) . x = TRUE iff ( p . x = TRUE & q . x = TRUE ) ) )
assume A1: x in (dom p) /\ (dom q) ; :: thesis: ( (p '&' q) . x = TRUE iff ( p . x = TRUE & q . x = TRUE ) )
x in dom (p '&' q) by A1, MARGREL1:def 18;
then (p '&' q) . x = (p . x) '&' (q . x) by MARGREL1:def 18;
hence ( (p '&' q) . x = TRUE iff ( p . x = TRUE & q . x = TRUE ) ) by MARGREL1:12; :: thesis: verum