thus ( f is disjoint_valued implies for n, m being Element of NAT st n < m holds
f . n misses f . m ) by PROB_2:def 2; :: thesis: ( ( for n, m being Element of NAT st n < m holds
f . n misses f . m ) implies f is disjoint_valued )
assume A1: for n, m being Element of NAT st n < m holds
f . n misses f . m ; :: thesis: f is disjoint_valued

now :: thesis: for x, y being object st x <> y holds
f . x misses f . y

let x, y be object ; :: thesis: ( x <> y implies f . b₁ misses f . b₂ )
assume A2: x <> y ; :: thesis: f . b₁ misses f . b₂

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 . b₁ misses f . b₂

then reconsider n = x, m = y as Element of NAT by FUNCT_2:def 1;
( n < m or n > m ) by A2, XXREAL_0:1;
hence f . x misses f . y by A1; :: thesis: verum

end;

suppose ( not x in dom f or not y in dom f ) ; :: thesis: f . b₁ misses f . b₂

then ( f . x = {} or f . y = {} ) by FUNCT_1:def 2;
hence f . x misses f . y by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

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