consider F being Function of NAT,{{}} such that
A1: for n being Element of NAT holds F . n = {} by Th35;
{} in S by PROB_1:4;
then {{}} c= S by ZFMISC_1:31;
then reconsider F = F as Function of NAT,S by FUNCT_2:7;
take F ; :: thesis: F is disjoint_valued
A2: for n being set holds F . n = {}

proof

let n be set ; :: 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 set st x <> y holds
F . x misses F . y :: according to PROB_2:def 2 :: thesis: verum

proof

let x, y be set ; :: thesis: ( x <> y implies F . x misses F . y )
F . x = {} by A2;
hence ( x <> y implies F . x misses F . y ) by XBOOLE_1:65; :: thesis: verum

end;