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

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

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

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

suppose ( x in dom A1 & y in dom A1 ) ; :: thesis: A1 . b₁ misses A1 . b₂

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

end;

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

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

end;

end;

end;

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