let x, y be set ; :: thesis: dom <*x,y*> = Seg 2
thus dom <*x,y*> = Seg (len <*x,y*>) by FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44 ; :: thesis: verum