let n be Ordinal; :: thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for x being Function of n,L holds eval ((0_ (n,L)),x) = 0. L
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for x being Function of n,L holds eval ((0_ (n,L)),x) = 0. L
let x be Function of n,L; :: thesis: eval ((0_ (n,L)),x) = 0. L
set 0p = 0_ (n,L);
consider y being FinSequence of the carrier of L such that
A1: len y = len (SgmX ((BagOrder n),(Support (0_ (n,L))))) and
A2: Sum y = eval ((0_ (n,L)),x) and
for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (((0_ (n,L)) * (SgmX ((BagOrder n),(Support (0_ (n,L)))))) /. i) * (eval (((SgmX ((BagOrder n),(Support (0_ (n,L))))) /. i),x)) by Def2;
Support (0_ (n,L)) = {}
proof
set u = the Element of Support (0_ (n,L));
assume Support (0_ (n,L)) <> {} ; :: thesis: contradiction
then A3: the Element of Support (0_ (n,L)) in Support (0_ (n,L)) ;
then A4: the Element of Support (0_ (n,L)) is Element of Bags n ;
(0_ (n,L)) . the Element of Support (0_ (n,L)) <> 0. L by A3, POLYNOM1:def 4;
hence contradiction by A4, POLYNOM1:22; :: thesis: verum
end;
then SgmX ((BagOrder n),(Support (0_ (n,L)))) = {} by Th10, PRE_POLY:76;
then y = <*> the carrier of L by A1;
hence eval ((0_ (n,L)),x) = 0. L by A2, RLVECT_1:43; :: thesis: verum