let x be set ; :: thesis: <*x*> is one-to-one
let y1 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not y1 in proj1 <*x*> or not b₁ in proj1 <*x*> or not <*x*> . y1 = <*x*> . b₁ or y1 = b₁ )
let y2 be set ; :: thesis: ( not y1 in proj1 <*x*> or not y2 in proj1 <*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:4, FINSEQ_1:def 8;
then A3: y1 = 1 by TARSKI:def 1;
y2 in {1} by A2, FINSEQ_1:4, FINSEQ_1:def 8;
hence y1 = y2 by A3, TARSKI:def 1; :: thesis: verum