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