:: deftheorem defines |^ YELLOW_1:def 5 :
for I being set
for T being RelStr holds T |^ I = product (I --> T);