let X be non empty Ordinal; :: thesis: for x being Element of X
for L being 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 trivial well-unital doubleLoopStr
for e being Function of X,L holds eval ((UnitBag x),e) = e . x
let L be 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:15
.= (power L) . ((e . x),(0 + 1)) by Th9
.= ((power L) . (edx,0)) * edx by GROUP_1:def 7
.= (1_ L) * edx by GROUP_1:def 7
.= e . x ;
:: thesis: verum