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