{} 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 . b1 misses F . b2 )
assume i <> j ; :: thesis: F . b1 misses F . b2
per cases ( i in dom F or not i in dom F ) ;
end;
end;
hence F is disjoint_valued by PROB_2:def 2; :: thesis: verum