let x be object ; :: thesis:

let i, j be object ; :: thesis:
assume A1: i <> j ; :: thesis:
A2: dom <*x*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

suppose i in dom <*x*> ; :: thesis:

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:

end;

suppose not i in dom <*x*> ; :: thesis:

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

end;

end;

end;

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