consider f being Function of NAT ,{{} } such that
A1: for n being Element of NAT holds f . n = {} by MEASURE1:35;
{} in F by PROB_1:10;
then {{} } c= F by ZFMISC_1:37;
then reconsider f = f as Function of NAT ,F by FUNCT_2:9;
take f ; :: thesis: f is disjoint_valued
A2: for x being set holds f . x = {}

proof

let x be set ; :: thesis: f . x = {}
( x in dom f implies f . x = {} ) by A1;
hence f . x = {} by FUNCT_1:def 4; :: thesis: verum

end;

thus for x, y being set st x <> y holds
f . x misses f . y :: according to PROB_2:def 3 :: thesis: verum

proof

let x, y be set ; :: thesis: ( x <> y implies f . x misses f . y )
( f . x = {} & f . y = {} ) by A2;
hence ( x <> y implies f . x misses f . y ) by XBOOLE_1:65; :: thesis: verum

end;