:: deftheorem Def12 defines product" CARD_3:def 12 :
for S being functional set
for b₂ being Function holds
( b₂ = product" S iff ( dom b₂ = DOM S & ( for i being set st i in dom b₂ holds
b₂ . i = pi (S,i) ) ) );