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 dom <*x*> or not b₁ in dom <*x*> or not <*x*> . y1 = <*x*> . b₁ or y1 = b₁ )
let y2 be set ; :: thesis: ( not y1 in dom <*x*> or not y2 in dom <*x*> or not <*x*> . y1 = <*x*> . y2 or y1 = y2 )
assume ( y1 in dom <*x*> & y2 in dom <*x*> & <*x*> . y1 = <*x*> . y2 ) ; :: thesis: y1 = y2
then ( y1 in {1} & y2 in {1} ) by FINSEQ_1:4, FINSEQ_1:def 8;
then ( y1 = 1 & y2 = 1 ) by TARSKI:def 1;
hence y1 = y2 ; :: thesis: verum