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

proof

let n be object ; :: thesis: F . n = {}

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

suppose n in dom F ; :: thesis: F . n = {}

hence F . n = {} by A1; :: thesis: verum

end;

suppose not n in dom F ; :: thesis: F . n = {}

hence F . n = {} by FUNCT_1:def 2; :: thesis: verum

end;

end;

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 ) ; :: thesis: verum

end;