let A, B be Ring; :: thesis: for x being Element of B holds Ext_eval ((0_. A),x) = 0. B
let x be Element of B; :: thesis: Ext_eval ((0_. A),x) = 0. B
consider F being FinSequence of B such that
A1: Ext_eval ((0_. A),x) = Sum F and
A2: len F = len (0_. A) and
for n being Element of NAT st n in dom F holds
F . n = (In (((0_. A) . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) by Def1;
F = <*> the carrier of B by A2, POLYNOM4:3;
hence Ext_eval ((0_. A),x) = 0. B by A1, RLVECT_1:43; :: thesis: verum