theorem Th19: :: HILB10_2:19

for O being Ordinal
for L being non trivial associative commutative well-unital doubleLoopStr
for x being Function of O,L
for b being bag of O
for S being one-to-one FinSequence of O st rng S = support b holds
ex y being FinSequence of L st
( len y = card (support b) & eval (b,x) = Product y & ( for i being Nat st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * S) /. i),((b * S) /. i)) ) )