theorem Th23: :: JORDAN23:23

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