len <*x,y*> = 2 by FINSEQ_1:44;
hence <*x,y*> is poorly-one-to-one by Def3; :: thesis: verum