consider F being sequence of {{}} such that

A1: for n being Element of NAT holds F . n = {} by Th16;

{} in S by PROB_1:4;

then {{}} c= S by ZFMISC_1:31;

then reconsider F = F as sequence of S by FUNCT_2:7;

take F ; :: thesis: F is disjoint_valued

A2: for n being object holds F . n = {} thus for x, y being object st x <> y holds

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

A1: for n being Element of NAT holds F . n = {} by Th16;

{} in S by PROB_1:4;

then {{}} c= S by ZFMISC_1:31;

then reconsider F = F as sequence of S by FUNCT_2:7;

take F ; :: thesis: F is disjoint_valued

A2: for n being object holds F . n = {} thus for x, y being object st x <> y holds

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