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

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