let D be non empty set ; for p, q being PartialPredicate of D holds PP_and (p,(PP_or (p,q))) = p
let p, q be PartialPredicate of D; PP_and (p,(PP_or (p,q))) = p
set o = PP_or (p,q);
set a = PP_and (p,(PP_or (p,q)));
A1:
dom (PP_and (p,(PP_or (p,q)))) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = TRUE ) ) }
by Th16;
A2:
dom (PP_or (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) }
by Def4;
thus
dom (PP_and (p,(PP_or (p,q)))) = dom p
FUNCT_1:def 11 for b1 being object holds
( not b1 in dom (PP_and (p,(PP_or (p,q)))) or (PP_and (p,(PP_or (p,q)))) . b1 = p . b1 )proof
thus
dom (PP_and (p,(PP_or (p,q)))) c= dom p
XBOOLE_0:def 10 dom p c= dom (PP_and (p,(PP_or (p,q))))
let d be
object ;
TARSKI:def 3 ( not d in dom p or d in dom (PP_and (p,(PP_or (p,q)))) )
assume A5:
d in dom p
;
d in dom (PP_and (p,(PP_or (p,q))))
per cases then
( p . d = TRUE or p . d = FALSE )
by Th3;
suppose A6:
p . d = TRUE
;
d in dom (PP_and (p,(PP_or (p,q))))then A7:
(PP_or (p,q)) . d = TRUE
by A5, Def4;
d in dom (PP_or (p,q))
by A2, A5, A6;
hence
d in dom (PP_and (p,(PP_or (p,q))))
by A1, A5, A6, A7;
verum end; end;
end;
let d be object ; ( not d in dom (PP_and (p,(PP_or (p,q)))) or (PP_and (p,(PP_or (p,q)))) . d = p . d )
assume
d in dom (PP_and (p,(PP_or (p,q))))
; (PP_and (p,(PP_or (p,q)))) . d = p . d