theorem Th11: :: POLNOT_1:11

for P being FinSequence-membered set
for p, q being FinSequence
for m, n being Nat st p in P ^^ m & q in P ^^ n holds
p ^ q in P ^^ (m + n)