let x be object ; :: thesis: for D being non empty set

for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( not x in dom (PP_IF (p,f,g)) or ( x in dom p & p . x = TRUE & x in dom f ) or ( x in dom p & p . x = FALSE & x in dom g ) )

let D be non empty set ; :: thesis: for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( not x in dom (PP_IF (p,f,g)) or ( x in dom p & p . x = TRUE & x in dom f ) or ( x in dom p & p . x = FALSE & x in dom g ) )

let p be PartialPredicate of D; :: thesis: for f, g being BinominativeFunction of D holds

( not x in dom (PP_IF (p,f,g)) or ( x in dom p & p . x = TRUE & x in dom f ) or ( x in dom p & p . x = FALSE & x in dom g ) )

let f, g be BinominativeFunction of D; :: thesis: ( not x in dom (PP_IF (p,f,g)) or ( x in dom p & p . x = TRUE & x in dom f ) or ( x in dom p & p . x = FALSE & x in dom g ) )

assume A1: x in dom (PP_IF (p,f,g)) ; :: thesis: ( ( x in dom p & p . x = TRUE & x in dom f ) or ( x in dom p & p . x = FALSE & x in dom g ) )

dom (PP_IF (p,f,g)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE & d in dom f ) or ( d in dom p & p . d = FALSE & d in dom g ) ) } by Def13;

then ex d1 being Element of D st

( d1 = x & ( ( d1 in dom p & p . d1 = TRUE & d1 in dom f ) or ( d1 in dom p & p . d1 = FALSE & d1 in dom g ) ) ) by A1;

hence ( ( x in dom p & p . x = TRUE & x in dom f ) or ( x in dom p & p . x = FALSE & x in dom g ) ) ; :: thesis: verum

for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( not x in dom (PP_IF (p,f,g)) or ( x in dom p & p . x = TRUE & x in dom f ) or ( x in dom p & p . x = FALSE & x in dom g ) )

let D be non empty set ; :: thesis: for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( not x in dom (PP_IF (p,f,g)) or ( x in dom p & p . x = TRUE & x in dom f ) or ( x in dom p & p . x = FALSE & x in dom g ) )

let p be PartialPredicate of D; :: thesis: for f, g being BinominativeFunction of D holds

( not x in dom (PP_IF (p,f,g)) or ( x in dom p & p . x = TRUE & x in dom f ) or ( x in dom p & p . x = FALSE & x in dom g ) )

let f, g be BinominativeFunction of D; :: thesis: ( not x in dom (PP_IF (p,f,g)) or ( x in dom p & p . x = TRUE & x in dom f ) or ( x in dom p & p . x = FALSE & x in dom g ) )

assume A1: x in dom (PP_IF (p,f,g)) ; :: thesis: ( ( x in dom p & p . x = TRUE & x in dom f ) or ( x in dom p & p . x = FALSE & x in dom g ) )

dom (PP_IF (p,f,g)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE & d in dom f ) or ( d in dom p & p . d = FALSE & d in dom g ) ) } by Def13;

then ex d1 being Element of D st

( d1 = x & ( ( d1 in dom p & p . d1 = TRUE & d1 in dom f ) or ( d1 in dom p & p . d1 = FALSE & d1 in dom g ) ) ) by A1;

hence ( ( x in dom p & p . x = TRUE & x in dom f ) or ( x in dom p & p . x = FALSE & x in dom g ) ) ; :: thesis: verum