let f, g be non-empty Function; :: thesis: ( dom g c= dom f & ( for i being object st i in dom g holds
g . i c= f . i ) implies product (f +* g) c= product f )

assume that
A1: dom g c= dom f and
A2: for i being object st i in dom g holds
g . i c= f . i ; :: thesis: product (f +* g) c= product f
A3: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1
.= dom f by ;
now :: thesis: for x being object st x in dom (f +* g) holds
(f +* g) . x c= f . x
let x be object ; :: thesis: ( x in dom (f +* g) implies (f +* g) . x c= f . x )
assume x in dom (f +* g) ; :: thesis: (f +* g) . x c= f . x
thus (f +* g) . x c= f . x :: thesis: verum
proof
let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in (f +* g) . x or i in f . x )
assume A4: i in (f +* g) . x ; :: thesis: i in f . x
per cases ( x in dom g or not x in dom g ) ;
suppose a5: x in dom g ; :: thesis: i in f . x
then A5: i in g . x by ;
g . x c= f . x by a5, A2;
hence i in f . x by A5; :: thesis: verum
end;
suppose not x in dom g ; :: thesis: i in f . x
hence i in f . x by ; :: thesis: verum
end;
end;
end;
end;
hence product (f +* g) c= product f by ; :: thesis: verum