thus ( F is disjoint_valued implies for m, n being Nat st m in dom F & n in dom F & m <> n holds
F . m misses F . n ) by PROB_2:def 2; :: thesis: ( ( for m, n being Nat st m in dom F & n in dom F & m <> n holds
F . m misses F . n ) implies F is disjoint_valued )
assume A1: for m, n being Nat st m in dom F & n in dom F & m <> n holds
F . m misses F . n ; :: thesis: F is disjoint_valued

now :: thesis: for m, n being object st m <> n holds
F . m misses F . n

let m, n be object ; :: thesis: ( m <> n implies F . b₁ misses F . b₂ )
assume A2: m <> n ; :: thesis: F . b₁ misses F . b₂

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

suppose ( not m in dom F or not n in dom F ) ; :: thesis: F . b₁ misses F . b₂

then ( F . m = {} or F . n = {} ) by FUNCT_1:def 2;
hence F . m misses F . n ; :: thesis: verum

end;

suppose ( m in dom F & n in dom F ) ; :: thesis: F . b₁ misses F . b₂

hence F . m misses F . n by A1, A2; :: thesis: verum

end;

end;

end;

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