let D be non empty set ; :: thesis: for p being PartialPredicate of D holds PP_and (p,(PP_False D)) = PP_False D
let p be PartialPredicate of D; :: thesis: PP_and (p,(PP_False D)) = PP_False D
set q = PP_False D;
set f = PP_and (p,(PP_False D));
A1: dom (PP_and (p,(PP_False D))) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (PP_False D) & (PP_False D) . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom (PP_False D) & (PP_False D) . d = TRUE ) ) } by Th16;
thus A3: dom (PP_and (p,(PP_False D))) = dom (PP_False D) :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (PP_and (p,(PP_False D))) or (PP_and (p,(PP_False D))) . b₁ = (PP_False D) . b₁ )

proof

thus dom (PP_and (p,(PP_False D))) c= dom (PP_False D) ; :: according to XBOOLE_0:def 10 :: thesis: dom (PP_False D) c= dom (PP_and (p,(PP_False D)))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (PP_False D) or x in dom (PP_and (p,(PP_False D))) )
assume x in dom (PP_False D) ; :: thesis: x in dom (PP_and (p,(PP_False D)))
then reconsider d = x as Element of D ;
(PP_False D) . d = FALSE ;
hence x in dom (PP_and (p,(PP_False D))) by A1; :: thesis: verum

end;

let x be object ; :: thesis: ( not x in dom (PP_and (p,(PP_False D))) or (PP_and (p,(PP_False D))) . x = (PP_False D) . x )
assume A5: x in dom (PP_and (p,(PP_False D))) ; :: thesis: (PP_and (p,(PP_False D))) . x = (PP_False D) . x
then (PP_False D) . x = FALSE by FUNCOP_1:7;
hence (PP_and (p,(PP_False D))) . x = (PP_False D) . x by A3, A5, Th19; :: thesis: verum