theorem Th1: :: HILB10_3:1

for O being non empty Ordinal
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