let n be Ordinal; :: thesis: for L being non empty non trivial well-unital doubleLoopStr
for x being Function of n,L holds eval (EmptyBag n),x = 1. L
let L be non empty 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 by Lm7;
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 Def2;
SgmX (RelIncl n),s = {} by Th9, Th15;
then y = <*> the carrier of L by A1;
then eval (EmptyBag n),x = 1_ L by A2, GROUP_4:11;
hence eval (EmptyBag n),x = 1. L ; :: thesis: verum