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 = {}

f . x misses f . y :: according to PROB_2:def 2 :: thesis: verum

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

thus
for x, y being object st x <> y holds
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;( x in dom f implies f . x = {} ) by A1;

hence f . x = {} by FUNCT_1:def 2; :: thesis: verum

f . x misses f . y :: according to PROB_2:def 2 :: thesis: verum