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