theorem Th43: :: TOPS_5:43

for f being non-empty Function
for X being set
for i being object st i in dom f & X c= f . i holds
(proj (f,i)) .: (product (f +* (i,X))) = X