let D be non empty set ; :: thesis: for f being BinominativeFunction of D
for p, q, r being PartialPredicate of D st <*p,f,r*> is SFHT of D & <*q,f,r*> is SFHT of D holds
<*(PP_or (p,q)),f,r*> is SFHT of D
let f be BinominativeFunction of D; :: thesis: for p, q, r being PartialPredicate of D st <*p,f,r*> is SFHT of D & <*q,f,r*> is SFHT of D holds
<*(PP_or (p,q)),f,r*> is SFHT of D
let p, q, r be PartialPredicate of D; :: thesis: ( <*p,f,r*> is SFHT of D & <*q,f,r*> is SFHT of D implies <*(PP_or (p,q)),f,r*> is SFHT of D )
set P = PP_or (p,q);
assume A1: ( <*p,f,r*> is SFHT of D & <*q,f,r*> is SFHT of D ) ; :: thesis: <*(PP_or (p,q)),f,r*> is SFHT of D
for d being Element of D st d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = TRUE & d in dom f & f . d in dom r holds
r . (f . d) = TRUE

proof

let d be Element of D; :: thesis: ( d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = TRUE & d in dom f & f . d in dom r implies r . (f . d) = TRUE )
assume ( d in dom (PP_or (p,q)) & (PP_or (p,q)) . d = TRUE ) ; :: thesis: ( not d in dom f or not f . d in dom r or r . (f . d) = TRUE )
then ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) by PARTPR_1:10;
hence ( not d in dom f or not f . d in dom r or r . (f . d) = TRUE ) by A1, Th11; :: thesis: verum

end;

then <*(PP_or (p,q)),f,r*> in SFHTs D ;
hence <*(PP_or (p,q)),f,r*> is SFHT of D ; :: thesis: verum