for A being finite Approximation_Space
for x being Element of A holds (MemberFunc (({} A),A)) . x = 0