let D be non empty set ; :: thesis: for p, q, r being PartialPredicate of D holds PP_or (p,(PP_or (q,r))) = PP_or ((PP_or (p,q)),r)
let p, q, r be PartialPredicate of D; :: thesis: PP_or (p,(PP_or (q,r))) = PP_or ((PP_or (p,q)),r)
set qr = PP_or (q,r);
set a = PP_or (p,(PP_or (q,r)));
set pq = PP_or (p,q);
set b = PP_or ((PP_or (p,q)),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_or (p,(PP_or (q,r)))) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = FALSE ) ) } by Def4;
A3: 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;
A4: dom (PP_or ((PP_or (p,q)),r)) = { d where d is Element of D : ( ( d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = TRUE ) or ( d in dom r & r . d = TRUE ) or ( d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = FALSE & d in dom r & r . d = FALSE ) ) } by Def4;
thus dom (PP_or (p,(PP_or (q,r)))) = dom (PP_or ((PP_or (p,q)),r)) :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (PP_or (p,(PP_or (q,r)))) or (PP_or (p,(PP_or (q,r)))) . b₁ = (PP_or ((PP_or (p,q)),r)) . b₁ )

proof

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

proof

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

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

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

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

end;

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

( ( 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 A5, Th8;

per cases then ( ( d in dom q & q . d = TRUE ) or ( d in dom r & r . d = TRUE ) ) by A6, Def4;

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

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

end;

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

hence d in dom (PP_or ((PP_or (p,q)),r)) by A4; :: thesis: verum

end;

end;

end;

suppose that A7: d in dom p and
A8: p . d = FALSE and
A9: d in dom (PP_or (q,r)) and
A10: (PP_or (q,r)) . d = FALSE ; :: thesis: d in dom (PP_or ((PP_or (p,q)),r))

A11: ( ( 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 A9, Th8;
then ( d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = FALSE ) by A3, A7, A8, A10, Def4;
hence d in dom (PP_or ((PP_or (p,q)),r)) by A4, A11, Th11; :: thesis: verum

end;

end;

end;

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

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

suppose that A12: d in dom (PP_or (p,q)) and
A13: (PP_or (p,q)) . d = TRUE ; :: thesis: d in dom (PP_or (p,(PP_or (q,r))))

( ( 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 A12, Th8;
then ( ( d in dom p & p . d = TRUE ) or ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = TRUE ) ) by A1, A13, Def4;
hence d in dom (PP_or (p,(PP_or (q,r)))) by A2; :: thesis: verum

end;

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

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

end;

suppose that A14: d in dom (PP_or (p,q)) and
A15: (PP_or (p,q)) . d = FALSE and
A16: d in dom r and
A17: r . d = FALSE ; :: thesis: d in dom (PP_or (p,(PP_or (q,r))))

A18: ( ( 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 A14, Th8;
then ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = FALSE ) by A1, A15, A16, A17, Def4;
hence d in dom (PP_or (p,(PP_or (q,r)))) by A2, A18, Def4; :: thesis: verum

end;

end;

end;

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

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

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

then A20: d in dom (PP_or (p,q)) by A3;
(PP_or (p,q)) . d = TRUE by A19, Def4;
hence (PP_or ((PP_or (p,q)),r)) . d = TRUE by A20, Def4
.= (PP_or (p,(PP_or (q,r)))) . d by A19, Def4 ;
:: thesis: verum

end;

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

then ( ( 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 Th8;
then ( ( d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = TRUE ) or ( d in dom r & r . d = TRUE ) ) by A3, A21, Def4;
hence (PP_or ((PP_or (p,q)),r)) . d = TRUE by Def4
.= (PP_or (p,(PP_or (q,r)))) . d by A21, Def4 ;
:: thesis: verum

end;

suppose that A22: ( d in dom p & p . d = FALSE ) and
A23: ( d in dom (PP_or (q,r)) & (PP_or (q,r)) . d = FALSE ) ; :: thesis: (PP_or (p,(PP_or (q,r)))) . d = (PP_or ((PP_or (p,q)),r)) . d

A24: ( ( 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 A23, Th8;
then ( d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = FALSE ) by A3, A22, A23, Def4;
hence (PP_or ((PP_or (p,q)),r)) . d = FALSE by A23, A24, Def4
.= (PP_or (p,(PP_or (q,r)))) . d by A22, A23, Def4 ;
:: thesis: verum

end;

end;