let x be object ; :: thesis: for D being set
for p being PartialPredicate of D
for f being BinominativeFunction of D st x in dom (PP_prediction (f,p)) holds
( x in dom (p * f) & ( (p * f) . x = TRUE or (p * f) . x = FALSE ) )
let D be set ; :: thesis: for p being PartialPredicate of D
for f being BinominativeFunction of D st x in dom (PP_prediction (f,p)) holds
( x in dom (p * f) & ( (p * f) . x = TRUE or (p * f) . x = FALSE ) )
let p be PartialPredicate of D; :: thesis: for f being BinominativeFunction of D st x in dom (PP_prediction (f,p)) holds
( x in dom (p * f) & ( (p * f) . x = TRUE or (p * f) . x = FALSE ) )
let f be BinominativeFunction of D; :: thesis: ( x in dom (PP_prediction (f,p)) implies ( x in dom (p * f) & ( (p * f) . x = TRUE or (p * f) . x = FALSE ) ) )
assume x in dom (PP_prediction (f,p)) ; :: thesis: ( x in dom (p * f) & ( (p * f) . x = TRUE or (p * f) . x = FALSE ) )
then x in dom (p * f) by D1;
hence ( x in dom (p * f) & ( (p * f) . x = TRUE or (p * f) . x = FALSE ) ) by PARTPR_1:3; :: thesis: verum