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 A1, XBOOLE_1:12 ;
A4: product (f +* g) = (product f) /\ (product (f +* g)) by A1, A2, Th23, XBOOLE_1:28;
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 A4, Th22
.= (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 A3, a5, YELLOW17:3
.= f . i by A5, FUNCT_4:11 ; :: thesis: verum