let x, y be object ; :: thesis: dom <*x,y*> = {1,2}
thus dom <*x,y*> = Seg (len <*x,y*>) by Def3
.= {1,2} by Th2, Th44 ; :: thesis: verum