let T be non empty TopSpace; :: thesis: for A, B being Subset of T
for n being Element of 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; :: thesis: for n being Element of NAT
for S being Drizzle of A,B,n holds S is Element of PFuncs DYADIC ,(bool the carrier of T)
let n be Element of NAT ; :: thesis: 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; :: thesis: S is Element of PFuncs DYADIC ,(bool the carrier of T)
dyadic n c= DYADIC by URYSOHN2:27;
then S is PartFunc of DYADIC ,(bool the carrier of T) by RELSET_1:17;
hence S is Element of PFuncs DYADIC ,(bool the carrier of T) by PARTFUN1:119; :: thesis: verum