theorem Th100: :: CARD_3:103

for I being set
for f being non-empty b₁ -defined Function
for p being b₁ -defined b₂ -compatible Function holds p in sproduct f