theorem Th34: :: FINSEQ_1:34

for p being FinSequence holds
( p ^ {} = p & {} ^ p = p )