let x be object ; :: thesis: <*x*> is one-to-one
let y1, y2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not y1 in dom <*x*> or not y2 in dom <*x*> or not <*x*> . y1 = <*x*> . y2 or y1 = y2 )
assume that
A1: y1 in dom <*x*> and
A2: y2 in dom <*x*> and
<*x*> . y1 = <*x*> . y2 ; :: thesis: y1 = y2
y1 in {1} by A1, FINSEQ_1:2, FINSEQ_1:def 8;
then A3: y1 = 1 by TARSKI:def 1;
y2 in {1} by A2, FINSEQ_1:2, FINSEQ_1:def 8;
hence y1 = y2 by A3, TARSKI:def 1; :: thesis: verum