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