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