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

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