:: deftheorem Def2 defines Product SRINGS_5:def 11 :
for n being Nat
for X, b₃ being set holds
( b₃ = Product (n,X) iff for f being object holds
( f in b₃ iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) ) );