let A, B be non degenerated comRing; :: thesis: for n being Ordinal
for x being Function of n,B holds Ext_eval ((0_ (n,A)),x) = 0. B
let n be Ordinal; :: thesis: for x being Function of n,B holds Ext_eval ((0_ (n,A)),x) = 0. B
let x be Function of n,B; :: thesis: Ext_eval ((0_ (n,A)),x) = 0. B
set p = 0_ (n,A);
consider y being FinSequence of the carrier of B such that
A: ( Ext_eval ((0_ (n,A)),x) = Sum y & len y = len (SgmX ((BagOrder n),(Support (0_ (n,A))))) & ( for i being Element of NAT st 1 <= i & i <= len y holds
y . i = (In ((((0_ (n,A)) * (SgmX ((BagOrder n),(Support (0_ (n,A)))))) . i),B)) * (eval (((SgmX ((BagOrder n),(Support (0_ (n,A))))) /. i),x)) ) ) by defeval;
field (BagOrder n) = Bags n by ORDERS_1:12;
then B: BagOrder n linearly_orders Support (0_ (n,A)) by ORDERS_1:37, ORDERS_1:38;
Support (0_ (n,A)) = {} by YY;
then card (Support (0_ (n,A))) = 0 ;
then y = <*> the carrier of B by A, B, PRE_POLY:11;
hence Ext_eval ((0_ (n,A)),x) = 0. B by A, RLVECT_1:43; :: thesis: verum