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 A1, XBOOLE_1:12 ;

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 A4, FUNCT_4:13;
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 A4, FUNCT_4:11; :: thesis: verum

end;

end;

end;

end;

hence product (f +* g) c= product f by A3, CARD_3:27; :: thesis: verum