theorem Th12: :: POLNOT_1:12

for P being FinSequence-membered set
for p, q being FinSequence st p in P * & q in P * holds
p ^ q in P *