for X being RealUnitarySpace
for S being non empty finite Subset of X
for F being Function of the carrier of X, the carrier of X st S c= dom F & ( for y1, y2 being Point of X st y1 in S & y2 in S & y1 <> y2 holds
the scalar of X . [(F . y1),(F . y2)] = 0 ) holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = the scalar of X . [(F . y),(F . y)] ) holds
for p being FinSequence of the carrier of X st p is one-to-one & rng p = S holds
the scalar of X . [( the addF of X "**" (Func_Seq (F,p))),( the addF of X "**" (Func_Seq (F,p)))] = addreal "**" (Func_Seq (H,p))