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 for i being object st i in (dom f) \ (dom g) holds
(proj (f,i)) .: (product (f +* g)) = f . i )

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: for i being object st i in (dom f) \ (dom g) holds
(proj (f,i)) .: (product (f +* g)) = f . i

A3: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1
.= dom f by ;
A4: product (f +* g) = () /\ (product (f +* g)) by ;
let i be object ; :: thesis: ( i in (dom f) \ (dom g) implies (proj (f,i)) .: (product (f +* g)) = f . i )
assume a5: i in (dom f) \ (dom g) ; :: thesis: (proj (f,i)) .: (product (f +* g)) = f . i
then A5: ( i in dom f & not i in dom g ) by XBOOLE_0:def 5;
thus (proj (f,i)) .: (product (f +* g)) = (proj ((f +* g),i)) .: (product (f +* g)) by
.= (proj ((f +* g),i)) .: (dom (proj ((f +* g),i))) by CARD_3:def 16
.= rng (proj ((f +* g),i)) by RELAT_1:113
.= (f +* g) . i by
.= f . i by ; :: thesis: verum