let D be non empty set ; for p being PartialPredicate of D holds PP_or (p,(PP_True D)) = PP_True D
let p be PartialPredicate of D; 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)
FUNCT_1:def 11 for b1 being object holds
( not b1 in dom (PP_or (p,(PP_True D))) or (PP_or (p,(PP_True D))) . b1 = (PP_True D) . b1 )
let x be object ; ( 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)))
; (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; verum