:: deftheorem Def10 defines Product_dom RANDOM_3:def 10 :
for D, b₂ being ManySortedSet of NAT holds
( b₂ = Product_dom D iff ( b₂ . 0 = D . 0 & ( for i being Nat holds b₂ . (i + 1) = [:(b₂ . i),(D . (i + 1)):] ) ) );