theorem Th7: :: CATALAN2:7

for p, q being XFinSequence of NAT st p is dominated_by_0 & q is dominated_by_0 holds
p ^ q is dominated_by_0