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 g holds
(proj (f,i)) .: (product (f +* g)) = g . 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 g holds
(proj (f,i)) .: (product (f +* g)) = g . 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 g implies (proj (f,i)) .: (product (f +* g)) = g . i )
assume A5: i in dom g ; :: thesis: (proj (f,i)) .: (product (f +* g)) = g . i
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 A1, A3, A5, YELLOW17:3
.= g . i by A5, FUNCT_4:13 ; :: thesis: verum