{} in P by SETFAM_1:def 8;
then reconsider F = NAT --> {} as Function of NAT,P by FUNCOP_1:46;
take F ; :: thesis: F is disjoint_valued

now :: thesis: for i, j being object st i <> j holds
F . i misses F . j

let i, j be object ; :: thesis: ( i <> j implies F . b₁ misses F . b₂ )
assume i <> j ; :: thesis: F . b₁ misses F . b₂

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

suppose i in dom F ; :: thesis: F . b₁ misses F . b₂

thus F . i misses F . j by XBOOLE_1:65; :: thesis: verum

end;

suppose not i in dom F ; :: thesis: F . b₁ misses F . b₂

thus F . i misses F . j by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

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