theorem :: JORDAN23:24

for f being non empty FinSequence
for g being FinSequence holds dom g c= dom (f ^' g)