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