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 ) ;
end;
end;
hence F is disjoint_valued by PROB_2:def 2; :: thesis: verum