let x be object ; :: thesis: for D being non empty set
for p, q being PartialPredicate of D
for f being BinominativeFunction of D holds
( not x in dom (PP_FH (p,f,q)) or ( x in dom p & p . x = FALSE ) or ( x in dom (q * f) & (q * f) . x = TRUE ) or ( x in dom p & p . x = TRUE & x in dom (q * f) & (q * f) . x = FALSE ) )
let D be non empty set ; :: thesis: for p, q being PartialPredicate of D
for f being BinominativeFunction of D holds
( not x in dom (PP_FH (p,f,q)) or ( x in dom p & p . x = FALSE ) or ( x in dom (q * f) & (q * f) . x = TRUE ) or ( x in dom p & p . x = TRUE & x in dom (q * f) & (q * f) . x = FALSE ) )
let p, q be PartialPredicate of D; :: thesis: for f being BinominativeFunction of D holds
( not x in dom (PP_FH (p,f,q)) or ( x in dom p & p . x = FALSE ) or ( x in dom (q * f) & (q * f) . x = TRUE ) or ( x in dom p & p . x = TRUE & x in dom (q * f) & (q * f) . x = FALSE ) )
let f be BinominativeFunction of D; :: thesis: ( not x in dom (PP_FH (p,f,q)) or ( x in dom p & p . x = FALSE ) or ( x in dom (q * f) & (q * f) . x = TRUE ) or ( x in dom p & p . x = TRUE & x in dom (q * f) & (q * f) . x = FALSE ) )
assume A1: x in dom (PP_FH (p,f,q)) ; :: thesis: ( ( x in dom p & p . x = FALSE ) or ( x in dom (q * f) & (q * f) . x = TRUE ) or ( x in dom p & p . x = TRUE & x in dom (q * f) & (q * f) . x = FALSE ) )
dom (PP_FH (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } by Def15;
then ex d1 being Element of D st
( d1 = x & ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom (q * f) & (q * f) . d1 = TRUE ) or ( d1 in dom p & p . d1 = TRUE & d1 in dom (q * f) & (q * f) . d1 = FALSE ) ) ) by A1;
hence ( ( x in dom p & p . x = FALSE ) or ( x in dom (q * f) & (q * f) . x = TRUE ) or ( x in dom p & p . x = TRUE & x in dom (q * f) & (q * f) . x = FALSE ) ) ; :: thesis: verum