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 & q ||= r & dom r c= dom q holds
<*p,f,r*> 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 & q ||= r & dom r c= dom q holds
<*p,f,r*> is SFHT of D
let p, q, r be PartialPredicate of D; :: thesis: ( <*p,f,q*> is SFHT of D & q ||= r & dom r c= dom q implies <*p,f,r*> is SFHT of D )
assume that
A1: <*p,f,q*> is SFHT of D and
A2: q ||= r and
A3: dom r c= dom q ; :: thesis: <*p,f,r*> is SFHT of D
for d being Element of D st d in dom p & p . 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 p & p . d = TRUE & d in dom f & f . d in dom r implies r . (f . d) = TRUE )
assume that
A4: d in dom p and
A5: p . d = TRUE and
A6: d in dom f and
A7: f . d in dom r ; :: thesis: r . (f . d) = TRUE
q . (f . d) = TRUE by A1, A3, A4, A5, A6, A7, Th11;
hence r . (f . d) = TRUE by A2, A3, A7; :: thesis: verum

end;

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