thus ( F is disjoint_valued implies for a, b being object st a in dom F & b in dom F & a <> b holds
F . a misses F . b ) by PROB_2:def 2; :: thesis: ( ( for a, b being object st a in dom F & b in dom F & a <> b holds
F . a misses F . b ) implies F is disjoint_valued )
assume A1: for i, j being object st i in dom F & j in dom F & i <> j holds
F . i misses F . j ; :: thesis: F is disjoint_valued
for x, y being object st x <> y holds
F . x misses F . y

proof

let x, y be object ; :: thesis: ( x <> y implies F . x misses F . y )
assume A2: x <> y ; :: thesis: F . x misses F . y

per cases ( ( x in dom F & y in dom F ) or not x in dom F or not y in dom F ) ;

suppose ( x in dom F & y in dom F ) ; :: thesis: F . x misses F . y

hence F . x misses F . y by A1, A2; :: thesis: verum

end;

suppose not x in dom F ; :: thesis: F . x misses F . y

then F . x = {} by FUNCT_1:def 2;
hence F . x misses F . y ; :: thesis: verum

end;

suppose not y in dom F ; :: thesis: F . x misses F . y

then F . y = {} by FUNCT_1:def 2;
hence F . x misses F . y ; :: thesis: verum

end;

end;

end;

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