theorem Th3: :: POLNOT_1:3

for P being FinSequence-membered set holds
( P ^ {{}} = P & {{}} ^ P = P )