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

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