let x, y be set ; :: thesis: dom <*x,y*> = Seg 2
len <*x,y*> = 2 by FINSEQ_1:61;
hence dom <*x,y*> = Seg 2 by FINSEQ_1:def 3; :: thesis: verum