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