theorem Th74: :: CARD_3:77

for S being functional with_common_domain set holds S c= product (product" S)