let n be Ordinal; :: thesis: for L being non trivial well-unital doubleLoopStr
for x being Function of n,L holds eval ((EmptyBag n),x) = 1. L
let L be non trivial well-unital doubleLoopStr ; :: thesis: for x being Function of n,L holds eval ((EmptyBag n),x) = 1. L
let x be Function of n,L; :: thesis: eval ((EmptyBag n),x) = 1. L
set b = EmptyBag n;
reconsider s = support (EmptyBag n) as empty Subset of n ;
consider y being FinSequence of the carrier of L such that
A1: len y = len (SgmX ((RelIncl n),(support (EmptyBag n)))) and
A2: eval ((EmptyBag n),x) = Product y and
for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support (EmptyBag n))))) /. i),(((EmptyBag n) * (SgmX ((RelIncl n),(support (EmptyBag n))))) /. i)) by Def1;
SgmX ((RelIncl n),s) = {} by PRE_POLY:76, PRE_POLY:82;
then y = <*> the carrier of L by A1;
then eval ((EmptyBag n),x) = 1_ L by A2, GROUP_4:8;
hence eval ((EmptyBag n),x) = 1. L ; :: thesis: verum