let f, g be non-empty Function; :: thesis: ( dom g = 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 g) = g . i )
assume that
A1: dom g = 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 g) = g . i
let i be object ; :: thesis: ( i in dom g implies (proj (f,i)) .: (product g) = g . i )
assume A3: i in dom g ; :: thesis: (proj (f,i)) .: (product g) = g . i
thus (proj (f,i)) .: (product g) = (proj (f,i)) .: (product (f +* g)) by A1, FUNCT_4:19
.= g . i by A1, A2, A3, Th25 ; :: thesis: verum