let P, p, q be PartialPredicate of D; :: thesis: ( P = (PPdisjunction D) . (p,q) implies P = (PPdisjunction D) . (q,p) )
assume A1: P = (PPdisjunction D) . (p,q) ; :: thesis: P = (PPdisjunction D) . (q,p)
set Q = (PPdisjunction D) . (q,p);
A2: dom P = { 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 A1, Def4;
A3: dom ((PPdisjunction D) . (q,p)) = { d where d is Element of D : ( ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = FALSE & d in dom p & p . d = FALSE ) ) } by Def4;
thus dom P = dom ((PPdisjunction D) . (q,p)) :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom P or P . b₁ = ((PPdisjunction D) . (q,p)) . b₁ )

proof

thus dom P c= dom ((PPdisjunction D) . (q,p)) :: according to XBOOLE_0:def 10 :: thesis: dom ((PPdisjunction D) . (q,p)) c= dom P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom P or x in dom ((PPdisjunction D) . (q,p)) )
assume x in dom P ; :: thesis: x in dom ((PPdisjunction D) . (q,p))
then ex d being Element of D st
( x = 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 A2;
hence x in dom ((PPdisjunction D) . (q,p)) by A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((PPdisjunction D) . (q,p)) or x in dom P )
assume x in dom ((PPdisjunction D) . (q,p)) ; :: thesis: x in dom P
then ex d being Element of D st
( x = d & ( ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = FALSE & d in dom p & p . d = FALSE ) ) ) by A3;
hence x in dom P by A2; :: thesis: verum

end;

let x be object ; :: thesis: ( not x in dom P or P . x = ((PPdisjunction D) . (q,p)) . x )
assume x in dom P ; :: thesis: P . x = ((PPdisjunction D) . (q,p)) . x
then consider d being Element of D such that
A4: x = d and
A5: ( ( 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 A2;

per cases ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & d in dom q & p . d = FALSE & q . d = FALSE ) ) by A5;

suppose A6: ( d in dom p & p . d = TRUE ) ; :: thesis: P . x = ((PPdisjunction D) . (q,p)) . x

hence P . x = TRUE by A1, A4, Def4
.= ((PPdisjunction D) . (q,p)) . x by A4, A6, Def4 ;
:: thesis: verum

end;

suppose A7: ( d in dom q & q . d = TRUE ) ; :: thesis: P . x = ((PPdisjunction D) . (q,p)) . x

hence P . x = TRUE by A1, A4, Def4
.= ((PPdisjunction D) . (q,p)) . x by A4, A7, Def4 ;
:: thesis: verum

end;

suppose A8: ( d in dom p & d in dom q & p . d = FALSE & q . d = FALSE ) ; :: thesis: P . x = ((PPdisjunction D) . (q,p)) . x

hence P . x = FALSE by A1, A4, Def4
.= ((PPdisjunction D) . (q,p)) . x by A4, A8, Def4 ;
:: thesis: verum

end;

end;