let P, p, q be PartialPredicate of D; ( P = (PPdisjunction D) . (p,q) implies P = (PPdisjunction D) . (q,p) )
assume A1:
P = (PPdisjunction D) . (p,q)
; 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))
FUNCT_1:def 11 for b1 being object holds
( not b1 in dom P or P . b1 = ((PPdisjunction D) . (q,p)) . b1 )
let x be object ; ( not x in dom P or P . x = ((PPdisjunction D) . (q,p)) . x )
assume
x in dom P
; 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;