theorem Th14: :: PRVECT_1:14

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