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

proof

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

end;

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