consider F being sequence of {{}} such that
A1: for n being Element of NAT holds F . n = {} by MEASURE1:16;
{{}} c= P by ZFMISC_1:31, SETFAM_1:def 8;
then reconsider F = F as sequence of P by FUNCT_2:7;
take F ; :: thesis: F is disjoint_valued
for x, y being object st x <> y holds
F . x misses F . y

proof

let x, y be object ; :: thesis: ( x <> y implies F . x misses F . y )
assume x <> y ; :: thesis: F . x misses F . y

per cases ( x in dom F or not x in dom F ) ;

suppose x in dom F ; :: thesis: F . x misses F . y

then F . x = {} by A1;
hence F . x misses F . y by XBOOLE_1:65; :: thesis: verum

end;

suppose not x in dom F ; :: thesis: F . x misses F . y

then F . x = {} by FUNCT_1:def 2;
hence F . x misses F . y by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

hence F is disjoint_valued by PROB_2:def 2; :: thesis: verum