let a, b, c, d, e be object ; :: thesis: dom <*a,b,c,d,e*> = {1,2,3,4,5}
thus dom <*a,b,c,d,e*> = Seg (len <*a,b,c,d,e*>) by FINSEQ_1:def 3
.= {1,2,3,4,5} by FINSEQ_4:78, FINSEQ_3:3 ; :: thesis: verum