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;
consider y being FinSequence of the carrier of L such that
A1: ( len y = len (SgmX (RelIncl n),(support (EmptyBag n))) & eval (EmptyBag n),x = Product y & ( 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;
reconsider s = support (EmptyBag n) as empty Subset of n by Lm7;
SgmX (RelIncl n),s = {} by Th9, Th15;
then len (SgmX (RelIncl n),(support (EmptyBag n))) = 0 ;
then y = <*> the carrier of L by A1;
then eval (EmptyBag n),x = 1_ L by A1, GROUP_4:11;
hence eval (EmptyBag n),x = 1. L ; :: thesis: verum