let O be non empty Ordinal; :: thesis: for i being Element of O

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for x being Function of O,L holds eval ((1_1 (i,L)),x) = x . i

let i be Element of O; :: thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for x being Function of O,L holds eval ((1_1 (i,L)),x) = x . i

let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for x being Function of O,L holds eval ((1_1 (i,L)),x) = x . i

let x be Function of O,L; :: thesis: eval ((1_1 (i,L)),x) = x . i

set p = 1_1 (i,L);

Support (1_1 (i,L)) = {(UnitBag i)} by HILBASIS:13;

then eval ((1_1 (i,L)),x) = ((1_1 (i,L)) . (UnitBag i)) * (eval ((UnitBag i),x)) by POLYNOM2:19

.= (1_ L) * (eval ((UnitBag i),x)) by HILBASIS:12

.= eval ((UnitBag i),x) ;

hence eval ((1_1 (i,L)),x) = x . i by HILBASIS:11; :: thesis: verum

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for x being Function of O,L holds eval ((1_1 (i,L)),x) = x . i

let i be Element of O; :: thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for x being Function of O,L holds eval ((1_1 (i,L)),x) = x . i

let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for x being Function of O,L holds eval ((1_1 (i,L)),x) = x . i

let x be Function of O,L; :: thesis: eval ((1_1 (i,L)),x) = x . i

set p = 1_1 (i,L);

Support (1_1 (i,L)) = {(UnitBag i)} by HILBASIS:13;

then eval ((1_1 (i,L)),x) = ((1_1 (i,L)) . (UnitBag i)) * (eval ((UnitBag i),x)) by POLYNOM2:19

.= (1_ L) * (eval ((UnitBag i),x)) by HILBASIS:12

.= eval ((UnitBag i),x) ;

hence eval ((1_1 (i,L)),x) = x . i by HILBASIS:11; :: thesis: verum