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 ;

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

hence
product (f +* g) c= product f
by A3, CARD_3:27; :: thesis: verum(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

end;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

end;assume A4: i in (f +* g) . x ; :: thesis: i in f . x