let n be Ordinal; :: thesis: for L being non empty 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 empty 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 Def4;
Support (0_ n,L) = {}

proof

consider u being Element of Support (0_ n,L);
assume Support (0_ n,L) <> {} ; :: thesis: contradiction
then A3: u in Support (0_ n,L) ;
then A4: u is Element of Bags n ;
(0_ n,L) . u <> 0. L by A3, POLYNOM1:def 9;
hence contradiction by A4, POLYNOM1:81; :: thesis: verum

end;

then SgmX (BagOrder n),(Support (0_ n,L)) = {} by Th9, Th20;
then y = <*> the carrier of L by A1;
hence eval (0_ n,L),x = 0. L by A2, RLVECT_1:60; :: thesis: verum