let V, A be set ; :: thesis: for p, q being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A st ( for d being TypeSCNominativeData of V,A st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE ) holds
<*p,f,q*> is SFHT of (ND (V,A))
let p, q be SCPartialNominativePredicate of V,A; :: thesis: for f being SCBinominativeFunction of V,A st ( for d being TypeSCNominativeData of V,A st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE ) holds
<*p,f,q*> is SFHT of (ND (V,A))
let f be SCBinominativeFunction of V,A; :: thesis: ( ( for d being TypeSCNominativeData of V,A st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE ) implies <*p,f,q*> is SFHT of (ND (V,A)) )
assume A1: for d being TypeSCNominativeData of V,A st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE ; :: thesis: <*p,f,q*> is SFHT of (ND (V,A))
for d being Element of ND (V,A) st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE
proof
let d be Element of ND (V,A); :: thesis: ( d in dom p & p . d = TRUE & d in dom f & f . d in dom q implies q . (f . d) = TRUE )
d is TypeSCNominativeData of V,A by NOMIN_1:39;
hence ( d in dom p & p . d = TRUE & d in dom f & f . d in dom q implies q . (f . d) = TRUE ) by A1; :: thesis: verum
end;
then <*p,f,q*> in SFHTs (ND (V,A)) ;
hence <*p,f,q*> is SFHT of (ND (V,A)) ; :: thesis: verum