let X be non empty set ; :: thesis: for f, g being Function st rng g c= X holds
(X -indexing f) * g = ((id X) +* f) * g
let f, g be Function; :: thesis: ( rng g c= X implies (X -indexing f) * g = ((id X) +* f) * g )
assume A1: rng g c= X ; :: thesis: (X -indexing f) * g = ((id X) +* f) * g
dom (id X) = X by RELAT_1:71;
then ( dom ((id X) +* f) = X \/ (dom f) & X c= X \/ (dom f) ) by FUNCT_4:def 1, XBOOLE_1:7;
then ( rng g c= dom (X -indexing f) & rng g c= dom ((id X) +* f) ) by A1, PARTFUN1:def 4, XBOOLE_1:1;
then A2: ( dom ((X -indexing f) * g) = dom g & dom (((id X) +* f) * g) = dom g ) by RELAT_1:46;

now

let x be set ; :: thesis: ( x in dom g implies ((X -indexing f) * g) . x = (((id X) +* f) * g) . x )
assume x in dom g ; :: thesis: ((X -indexing f) * g) . x = (((id X) +* f) * g) . x
then ( ((X -indexing f) * g) . x = (X -indexing f) . (g . x) & (((id X) +* f) * g) . x = ((id X) +* f) . (g . x) & g . x in rng g ) by FUNCT_1:23, FUNCT_1:def 5;
hence ((X -indexing f) * g) . x = (((id X) +* f) * g) . x by A1, Th8; :: thesis: verum

end;

hence (X -indexing f) * g = ((id X) +* f) * g by A2, FUNCT_1:9; :: thesis: verum