let A be finite Approximation_Space; :: thesis: for x being Element of A holds (MemberFunc (({} A),A)) . x = 0
let x be Element of A; :: thesis: (MemberFunc (({} A),A)) . x = 0
UAp ({} A) = {} by Th19;
then (UAp ({} A)) ` = [#] A ;
hence (MemberFunc (({} A),A)) . x = 0 by Th41; :: thesis: verum