now :: thesis: for i, j being object st i <> j holds
<*x*> . i misses <*x*> . j

let i, j be object ; :: thesis: ( i <> j implies <*x*> . b₁ misses <*x*> . b₂ )
assume A3: i <> j ; :: thesis: <*x*> . b₁ misses <*x*> . b₂

per cases ( i in dom <*x*> or not i in dom <*x*> ) ;

suppose i in dom <*x*> ; :: thesis: <*x*> . b₁ misses <*x*> . b₂

then i in {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by TARSKI:def 1;
then not j in {1} by A3, TARSKI:def 1;
then not j in dom <*x*> by FINSEQ_1:2, FINSEQ_1:38;
then <*x*> . j = {} by FUNCT_1:def 2;
hence <*x*> . i misses <*x*> . j by XBOOLE_1:65; :: thesis: verum

end;

suppose not i in dom <*x*> ; :: thesis: <*x*> . b₁ misses <*x*> . b₂

then <*x*> . i = {} by FUNCT_1:def 2;
hence <*x*> . i misses <*x*> . j by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

hence <*x*> is disjoint_valued by PROB_2:def 2; :: thesis: verum