let f, g be non-empty Function; :: thesis: for x being Element of product (f +* g) holds x | (dom g) in product g
let x be Element of product (f +* g); :: thesis: x | (dom g) in product g
A1: dom x = dom (f +* g) by Th9;
A2: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
then A3: dom g c= dom x by A1, XBOOLE_1:7;
A4: dom (x | (dom g)) = dom g by A1, A2, RELAT_1:62, XBOOLE_1:7;
now :: thesis: for z being object st z in dom (x | (dom g)) holds
(x | (dom g)) . z in g . z
let z be object ; :: thesis: ( z in dom (x | (dom g)) implies (x | (dom g)) . z in g . z )
assume A5: z in dom (x | (dom g)) ; :: thesis: (x | (dom g)) . z in g . z
then A6: (x | (dom g)) . z = x . z by FUNCT_1:47;
(f +* g) . z = g . z by A4, A5, FUNCT_4:13;
hence (x | (dom g)) . z in g . z by A1, A3, A4, A5, A6, Th9; :: thesis: verum
end;
hence x | (dom g) in product g by A4, Th9; :: thesis: verum