theorem :: ALGSPEC1:22

for f, g being Function st dom f misses dom g & rng g misses dom f holds
for X being set holds f * (X -indexing g) = f | X