let X be non empty Ordinal; :: thesis: for x being Element of X
for L being non empty non trivial well-unital doubleLoopStr
for e being Function of X,L holds eval (UnitBag x),e = e . x
let x be Element of X; :: thesis: for L being non empty non trivial well-unital doubleLoopStr
for e being Function of X,L holds eval (UnitBag x),e = e . x
let L be non empty non trivial well-unital doubleLoopStr ; :: thesis: for e being Function of X,L holds eval (UnitBag x),e = e . x
let e be Function of X,L; :: thesis: eval (UnitBag x),e = e . x
reconsider edx = e . x as Element of L ;
support (UnitBag x) = {x} by Th8;
hence eval (UnitBag x),e = (power L) . (e . x),((UnitBag x) . x) by POLYNOM2:17
.= (power L) . (e . x),(0 + 1) by Th9
.= ((power L) . edx,0 ) * edx by GROUP_1:def 8
.= (1_ L) * edx by GROUP_1:def 8
.= e . x by GROUP_1:def 5 ;
:: thesis: verum