thus
( A1 is V77() 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

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

hence
A1 is disjoint_valued
by PROB_2:def 2; :: thesis: verumA1 . x misses A1 . y

let x, y be object ; :: thesis: ( x <> y implies A1 . b_{1} misses A1 . b_{2} )

assume A2: x <> y ; :: thesis: A1 . b_{1} misses A1 . b_{2}

end;assume A2: x <> y ; :: thesis: A1 . b