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