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;
A2: ex gg being Function st
( x = gg & dom gg = dom M & ( for x being object st x in dom M holds
gg . x in M . x ) ) by A1, Def5;
then A3: dom (x * g) = dom (M * g) by RELAT_1:163;
now :: thesis: for y being object st y in dom (M * g) holds
(x * g) . y in (M * g) . y
let y be object ; :: thesis: ( y in dom (M * g) implies (x * g) . y in (M * g) . y )
assume A4: y in dom (M * g) ; :: thesis: (x * g) . y in (M * g) . y
then A5: y in dom g by FUNCT_1:11;
A6: g . y in dom M by A4, FUNCT_1:11;
A7: (x * g) . y = x . (g . y) by A5, FUNCT_1:13;
(M * g) . y = M . (g . y) by A5, FUNCT_1:13;
hence (x * g) . y in (M * g) . y by A2, A6, A7; :: thesis: verum
end;
hence x * g in product (M * g) by A3, Def5; :: thesis: verum