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
rng g c= dom (X -indexing f) by A1, PARTFUN1:def 2;
then A2: dom ((X -indexing f) * g) = dom g by RELAT_1:27;

A3: now :: thesis: for x being object st x in dom g holds
((X -indexing f) * g) . x = (((id X) +* f) * g) . x

let x be object ; :: thesis: ( x in dom g implies ((X -indexing f) * g) . x = (((id X) +* f) * g) . x )
assume A4: x in dom g ; :: thesis: ((X -indexing f) * g) . x = (((id X) +* f) * g) . x
then A5: (((id X) +* f) * g) . x = ((id X) +* f) . (g . x) by FUNCT_1:13;
A6: g . x in rng g by A4, FUNCT_1:def 3;
((X -indexing f) * g) . x = (X -indexing f) . (g . x) by A4, FUNCT_1:13;
hence ((X -indexing f) * g) . x = (((id X) +* f) * g) . x by A1, A5, A6, Th8; :: thesis: verum

end;

dom (id X) = X ;
then A7: dom ((id X) +* f) = X \/ (dom f) by FUNCT_4:def 1;
X c= X \/ (dom f) by XBOOLE_1:7;
then dom (((id X) +* f) * g) = dom g by A1, A7, RELAT_1:27, XBOOLE_1:1;
hence (X -indexing f) * g = ((id X) +* f) * g by A2, A3; :: thesis: verum