for D being ManySortedSet of NAT holds
( (Product_dom D) . 0 = D . 0 & (Product_dom D) . 1 = [:(D . 0),(D . 1):] & (Product_dom D) . 2 = [:(D . 0),(D . 1),(D . 2):] & (Product_dom D) . 3 = [:(D . 0),(D . 1),(D . 2),(D . 3):] )