let f, g be non-empty Function; :: thesis: for x being Element of product f
for y being Element of product g holds x +* y in product (f +* g)
let x be Element of product f; :: thesis: for y being Element of product g holds x +* y in product (f +* g)
let y be Element of product g; :: thesis: x +* y in product (f +* g)
A1: dom x = dom f by Th9;
A2: dom y = dom g by Th9;
then A3: dom (x +* y) = (dom f) \/ (dom g) by A1, FUNCT_4:def 1;
A4: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;

now :: thesis: for z being object st z in dom (f +* g) holds
(x +* y) . z in (f +* g) . z

let z be object ; :: thesis: ( z in dom (f +* g) implies (x +* y) . z in (f +* g) . z )
assume A5: z in dom (f +* g) ; :: thesis: (x +* y) . z in (f +* g) . z
then ( z in dom g or ( not z in dom g & z in dom f ) ) by A4, XBOOLE_0:def 3;
then ( ( (x +* y) . z = x . z & (f +* g) . z = f . z & x . z in f . z ) or ( (x +* y) . z = y . z & (f +* g) . z = g . z & y . z in g . z ) ) by A1, A2, A4, A5, Th9, FUNCT_4:def 1;
hence (x +* y) . z in (f +* g) . z ; :: thesis: verum

end;

hence x +* y in product (f +* g) by A3, A4, Th9; :: thesis: verum