let x1, x2, x3, x4 be set ; :: thesis: dom <*x1,x2,x3,x4*> = Seg 4
len <*x1,x2,x3,x4*> = 4 by Th91;
hence dom <*x1,x2,x3,x4*> = Seg 4 by FINSEQ_1:def 3; :: thesis: verum