let x be object ; :: thesis: <*x*> is disjoint_valued FinSequence

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 A1: i <> j ; :: thesis: <*x*> . b₁ misses <*x*> . b₂
A2: dom <*x*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

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 = 1 by A2, TARSKI:def 1;
then not j in {1} by A1, TARSKI:def 1;
then <*x*> . j = {} by A2, FUNCT_1:def 2;
hence <*x*> . i misses <*x*> . j ; :: 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 ; :: thesis: verum

end;

end;

end;

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