theorem Th21: :: TOPS_5:21

for f, g being non-empty Function
for i, x being object st x in (product f) /\ (product (f +* g)) holds
(proj (f,i)) . x = (proj ((f +* g),i)) . x