theorem :: TOPREAL7:3

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