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

proof

thus dom (PP_and (p,(PP_or (q,r)))) c= dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) :: according to XBOOLE_0:def 10 :: thesis: dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) c= dom (PP_and (p,(PP_or (q,r))))

proof

let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in dom (PP_and (p,(PP_or (q,r)))) or d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) )
assume d in dom (PP_and (p,(PP_or (q,r)))) ; :: thesis: d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r))))

per cases then ( ( d in dom p & p . d = FALSE ) or ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) ) by Th17;

suppose ( d in dom p & p . d = FALSE ) ; :: thesis: d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r))))

then ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = FALSE ) by A3, A4, Th19;
hence d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) by A5; :: thesis: verum

end;

suppose ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = FALSE ) ; :: thesis: d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r))))

then ( d in dom q & q . d = FALSE & d in dom r & r . d = FALSE ) by Th13;
then ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = FALSE ) by A3, A4, Th19;
hence d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) by A5; :: thesis: verum

end;

suppose that A6: ( d in dom p & p . d = TRUE ) and
A7: ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) ; :: thesis: d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r))))

( ( d in dom q & q . d = TRUE ) or ( d in dom r & r . d = TRUE ) ) by A7, Th10;
then ( ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = TRUE ) or ( d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = TRUE ) ) by A3, A4, A6, Th18;
hence d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) by A5; :: thesis: verum

end;

end;

end;

let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) or d in dom (PP_and (p,(PP_or (q,r)))) )
assume d in dom (PP_or ((PP_and (p,q)),(PP_and (p,r)))) ; :: thesis: d in dom (PP_and (p,(PP_or (q,r))))

per cases then ( ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = TRUE ) or ( d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = TRUE ) or ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = FALSE ) ) by Th8;

suppose A8: ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = TRUE ) ; :: thesis: d in dom (PP_and (p,(PP_or (q,r))))

then A9: ( d in dom p & p . d = TRUE ) by Th23;
( d in dom q & q . d = TRUE ) by A8, Th23;
then ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) by A1, Def4;
hence d in dom (PP_and (p,(PP_or (q,r)))) by A2, A9; :: thesis: verum

end;

suppose A10: ( d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = TRUE ) ; :: thesis: d in dom (PP_and (p,(PP_or (q,r))))

then A11: ( d in dom p & p . d = TRUE ) by Th23;
( d in dom r & r . d = TRUE ) by A10, Th23;
then ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) by A1, Def4;
hence d in dom (PP_and (p,(PP_or (q,r)))) by A2, A11; :: thesis: verum

end;

suppose ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = FALSE ) ; :: thesis: d in dom (PP_and (p,(PP_or (q,r))))

then ( ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) ) & ( ( d in dom p & p . d = FALSE ) or ( d in dom r & r . d = FALSE ) ) ) by Th25;
then ( ( d in dom p & p . d = FALSE ) or ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = FALSE ) ) by A1, Def4;
hence d in dom (PP_and (p,(PP_or (q,r)))) by A2; :: thesis: verum

end;

end;

end;

let d be object ; :: thesis: ( not d in dom (PP_and (p,(PP_or (q,r)))) or (PP_and (p,(PP_or (q,r)))) . d = (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d )
assume d in dom (PP_and (p,(PP_or (q,r)))) ; :: thesis: (PP_and (p,(PP_or (q,r)))) . d = (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d

per cases then ( ( d in dom p & p . d = FALSE ) or ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) ) by Th17;

suppose A12: ( d in dom p & p . d = FALSE ) ; :: thesis: (PP_and (p,(PP_or (q,r)))) . d = (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d

then ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = FALSE ) by A3, A4, Th19;
hence (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d = FALSE by Def4
.= (PP_and (p,(PP_or (q,r)))) . d by A12, Th19 ;
:: thesis: verum

end;

suppose A13: ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = FALSE ) ; :: thesis: (PP_and (p,(PP_or (q,r)))) . d = (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d

then ( d in dom q & q . d = FALSE & d in dom r & r . d = FALSE ) by Th13;
then ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = FALSE ) by A3, A4, Th19;
hence (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d = FALSE by Def4
.= (PP_and (p,(PP_or (q,r)))) . d by A13, Th19 ;
:: thesis: verum

end;

suppose that A14: ( d in dom p & p . d = TRUE ) and
A15: ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) ; :: thesis: (PP_and (p,(PP_or (q,r)))) . d = (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d

( ( d in dom q & q . d = TRUE ) or ( d in dom r & r . d = TRUE ) ) by A15, Th10;
then ( ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = TRUE ) or ( d in dom (PP_and (p,r)) & (PP_and (p,r)) . d = TRUE ) ) by A3, A4, A14, Th18;
hence (PP_or ((PP_and (p,q)),(PP_and (p,r)))) . d = TRUE by Def4
.= (PP_and (p,(PP_or (q,r)))) . d by A14, A15, Th18 ;
:: thesis: verum

end;

end;