let T be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: 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: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; :: thesis: verum

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; :: thesis: 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; :: 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: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; :: thesis: verum