for a being Domain-Sequence
for u being UnOps of a holds
( doms u = a & product (rngs u) c= product a )