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

proof

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

end;

let x be object ; :: thesis: ( not x in dom (PP_or (p,(PP_True D))) or (PP_or (p,(PP_True D))) . x = (PP_True D) . x )
assume A5: x in dom (PP_or (p,(PP_True D))) ; :: thesis: (PP_or (p,(PP_True D))) . x = (PP_True D) . x
then (PP_True D) . x = TRUE by FUNCOP_1:7;
hence (PP_or (p,(PP_True D))) . x = (PP_True D) . x by A3, A5, Def4; :: thesis: verum