let M, x, g be Function; :: thesis: ( x in product M implies x * g in product (M * g) )
assume A1: x in product M ; :: thesis: x * g in product (M * g)
set xg = x * g;
set Mg = M * g;
consider gg being Function such that
A2: ( x = gg & dom gg = dom M ) and
A3: for x being set st x in dom M holds
gg . x in M . x by A1, Def5;
A4: dom (x * g) = dom (M * g) by A2, RELAT_1:198;

now

let y be set ; :: thesis: ( y in dom (M * g) implies (x * g) . y in (M * g) . y )
assume y in dom (M * g) ; :: thesis: (x * g) . y in (M * g) . y
then A5: ( y in dom g & g . y in dom M ) by FUNCT_1:21;
then ( (x * g) . y = x . (g . y) & (M * g) . y = M . (g . y) ) by FUNCT_1:23;
hence (x * g) . y in (M * g) . y by A2, A3, A5; :: thesis: verum

end;

hence x * g in product (M * g) by A4, Def5; :: thesis: verum