theorem Th34: :: MONOID_1:34

for x being set
for A being non empty set
for p being FinSequence of A holds dom ({x} |` (p ^ <*x*>)) = (dom ({x} |` p)) \/ {((len p) + 1)}