consider f being sequence of {{}} such that
A1: for n being Element of NAT holds f . n = {} by MEASURE1:16;
{} in F by PROB_1:4;
then {{}} c= F by ZFMISC_1:31;
then reconsider f = f as sequence of F by FUNCT_2:7;
take f ; :: thesis: f is disjoint_valued
A2: for x being object holds f . x = {}

proof

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

end;

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

proof

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

end;