let D be non empty set ; :: thesis: for p being PartialPredicate of D holds PP_and (p,(PP_not p)) = (PP_False D) | (dom p)
let p be PartialPredicate of D; :: thesis: PP_and (p,(PP_not p)) = (PP_False D) | (dom p)
set n = PP_not p;
set a = PP_and (p,(PP_not p));
set B = PP_False D;
set t = (PP_False D) | (dom p);
A1: dom (PP_not p) = dom p by Def2;
A2: dom (PP_and (p,(PP_not p))) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (PP_not p) & (PP_not p) . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom (PP_not p) & (PP_not p) . d = TRUE ) ) } by Th16;
dom (PP_False D) = D ;
then A3: dom ((PP_False D) | (dom p)) = dom p by RELAT_1:62;
thus A4: dom (PP_and (p,(PP_not p))) = dom ((PP_False D) | (dom p)) :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (PP_and (p,(PP_not p))) or (PP_and (p,(PP_not p))) . b₁ = ((PP_False D) | (dom p)) . b₁ )

proof

thus dom (PP_and (p,(PP_not p))) c= dom ((PP_False D) | (dom p)) by A1, A3, Th17; :: according to XBOOLE_0:def 10 :: thesis: dom ((PP_False D) | (dom p)) c= dom (PP_and (p,(PP_not p)))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((PP_False D) | (dom p)) or x in dom (PP_and (p,(PP_not p))) )
assume A5: x in dom ((PP_False D) | (dom p)) ; :: thesis: x in dom (PP_and (p,(PP_not p)))

per cases then ( p . x = FALSE or p . x = TRUE ) by A3, Th3;

suppose p . x = FALSE ; :: thesis: x in dom (PP_and (p,(PP_not p)))

hence x in dom (PP_and (p,(PP_not p))) by A2, A3, A5; :: thesis: verum

end;

suppose p . x = TRUE ; :: thesis: x in dom (PP_and (p,(PP_not p)))

then (PP_not p) . x = FALSE by A3, A5, Def2;
hence x in dom (PP_and (p,(PP_not p))) by A1, A2, A3, A5; :: thesis: verum

end;

end;

end;

let x be object ; :: thesis: ( not x in dom (PP_and (p,(PP_not p))) or (PP_and (p,(PP_not p))) . x = ((PP_False D) | (dom p)) . x )
assume A6: x in dom (PP_and (p,(PP_not p))) ; :: thesis: (PP_and (p,(PP_not p))) . x = ((PP_False D) | (dom p)) . x
then A7: FALSE = (PP_False D) . x by FUNCOP_1:7
.= ((PP_False D) | (dom p)) . x by A3, A4, A6, FUNCT_1:49 ;

per cases ( p . x = FALSE or p . x = TRUE ) by A3, A4, A6, Th3;

suppose p . x = FALSE ; :: thesis: (PP_and (p,(PP_not p))) . x = ((PP_False D) | (dom p)) . x

hence (PP_and (p,(PP_not p))) . x = ((PP_False D) | (dom p)) . x by A3, A4, A6, A7, Th19; :: thesis: verum

end;

suppose p . x = TRUE ; :: thesis: (PP_and (p,(PP_not p))) . x = ((PP_False D) | (dom p)) . x

then (PP_not p) . x = FALSE by A3, A4, A6, Def2;
hence (PP_and (p,(PP_not p))) . x = ((PP_False D) | (dom p)) . x by A1, A3, A4, A6, A7, Th19; :: thesis: verum

end;

end;