let D be non empty set ; :: thesis: for f being BinominativeFunction of D
for p, q being PartialPredicate of D st <*p,f,q*> in SFHTs D holds
for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE
let f be BinominativeFunction of D; :: thesis: for p, q being PartialPredicate of D st <*p,f,q*> in SFHTs D holds
for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE
let p, q be PartialPredicate of D; :: thesis: ( <*p,f,q*> in SFHTs D implies for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE )
assume <*p,f,q*> in SFHTs D ; :: thesis: for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE
then consider p1, q1 being PartialPredicate of D, f1 being BinominativeFunction of D such that
A1: <*p,f,q*> = <*p1,f1,q1*> and
A2: for d being Element of D st d in dom p1 & p1 . d = TRUE & d in dom f1 & f1 . d in dom q1 holds
q1 . (f1 . d) = TRUE ;
( p = p1 & q = q1 & f = f1 ) by A1, FINSEQ_1:78;
hence for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE by A2; :: thesis: verum