let T be non empty TopSpace; for A, B being Subset of T
for n being Nat
for S being Drizzle of A,B,n holds S is Element of PFuncs (DYADIC,(bool the carrier of T))
let A, B be Subset of T; for n being Nat
for S being Drizzle of A,B,n holds S is Element of PFuncs (DYADIC,(bool the carrier of T))
let n be Nat; for S being Drizzle of A,B,n holds S is Element of PFuncs (DYADIC,(bool the carrier of T))
let S be Drizzle of A,B,n; S is Element of PFuncs (DYADIC,(bool the carrier of T))
dyadic n c= DYADIC
by URYSOHN2:23;
then
S is PartFunc of DYADIC,(bool the carrier of T)
by RELSET_1:7;
hence
S is Element of PFuncs (DYADIC,(bool the carrier of T))
by PARTFUN1:45; verum