theorem Th35: :: MONOID_1:35

for x, y being set
for A being non empty set
for p being FinSequence of A st x <> y holds
dom ({x} |` (p ^ <*y*>)) = dom ({x} |` p)