:: deftheorem defines setop_xPre_PROD BHSP_5:def 6 :
for X being RealUnitarySpace
for x being Point of X
for Y being finite Subset of X
for b₄ being Real holds
( b₄ = setop_xPre_PROD (x,Y,X) iff ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Nat st i in dom q holds
q . i = PO (i,p,x) ) & b₄ = addreal "**" q ) ) );