theorem Th28: :: E_TRANS1:28

for F being FinSequence of the carrier of (Polynom-Ring INT.Ring)
for x being Element of INT.Ring
for x1 being Element of F_Real st x = x1 holds
eval ((^ F),x1) = eval (F,x)