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;
Support (0_ n,L) = {}

proof

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

end;

then A3: SgmX (BagOrder n),(Support (0_ n,L)) = {} by Th9, Th20;
consider y being FinSequence of the carrier of L such that
A4: ( len y = len (SgmX (BagOrder n),(Support (0_ n,L))) & Sum y = eval (0_ n,L),x & ( 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;
len y = 0 by A3, A4;
then y = <*> the carrier of L ;
hence eval (0_ n,L),x = 0. L by A4, RLVECT_1:60; :: thesis: verum