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