let P be PartialPredicate of D; :: thesis: P = (PPdisjunction D) . (P,P)
set Q = (PPdisjunction D) . (P,P);
A9: dom ((PPdisjunction D) . (P,P)) = { d where d is Element of D : ( ( d in dom P & P . d = TRUE ) or ( d in dom P & P . d = TRUE ) or ( d in dom P & P . d = FALSE & d in dom P & P . d = FALSE ) ) } by Def4;
thus dom ((PPdisjunction D) . (P,P)) = dom P :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom P or P . b1 = ((PPdisjunction D) . (P,P)) . b1 )
proof
thus dom ((PPdisjunction D) . (P,P)) c= dom P :: according to XBOOLE_0:def 10 :: thesis: dom P c= dom ((PPdisjunction D) . (P,P))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((PPdisjunction D) . (P,P)) or x in dom P )
assume x in dom ((PPdisjunction D) . (P,P)) ; :: thesis: x in dom P
then ex d being Element of D st
( x = d & ( ( d in dom P & P . d = TRUE ) or ( d in dom P & P . d = TRUE ) or ( d in dom P & P . d = FALSE & d in dom P & P . d = FALSE ) ) ) by A9;
hence x in dom P ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom P or x in dom ((PPdisjunction D) . (P,P)) )
assume A10: x in dom P ; :: thesis: x in dom ((PPdisjunction D) . (P,P))
then ( P . x = TRUE or P . x = FALSE ) by Th3;
hence x in dom ((PPdisjunction D) . (P,P)) by A9, A10; :: thesis: verum
end;
let x be object ; :: thesis: ( not x in dom P or P . x = ((PPdisjunction D) . (P,P)) . x )
assume A11: x in dom P ; :: thesis: P . x = ((PPdisjunction D) . (P,P)) . x
then ( P . x = TRUE or P . x = FALSE ) by Th3;
hence P . x = ((PPdisjunction D) . (P,P)) . x by A11, Def4; :: thesis: verum