let A be finite discrete Approximation_Space; :: thesis: for X being Subset of A holds MemberFunc X,A = chi X,the carrier of A
let X be Subset of A; :: thesis: MemberFunc X,A = chi X,the carrier of A
reconsider F = MemberFunc X,A as Function of the carrier of A,REAL ;
set G = chi X,the carrier of A;
{0 ,1} c= REAL ;
then reconsider G = chi X,the carrier of A as Function of the carrier of A,REAL by FUNCT_2:9;
for x being set st x in the carrier of A holds
F . x = G . x

proof

let x be set ; :: thesis: ( x in the carrier of A implies F . x = G . x )
assume A1: x in the carrier of A ; :: thesis: F . x = G . x

per cases ( x in X or not x in X ) ;

suppose A2: x in X ; :: thesis: F . x = G . x

then x in LAp X by Th15;
then F . x = 1 by Th40;
hence F . x = G . x by A2, FUNCT_3:def 3; :: thesis: verum

end;

suppose A3: not x in X ; :: thesis: F . x = G . x

then not x in UAp X by Th16;
then x in (UAp X) ` by A1, XBOOLE_0:def 5;
then F . x = 0 by Th41;
hence F . x = G . x by A1, A3, FUNCT_3:def 3; :: thesis: verum

end;

end;

end;

hence MemberFunc X,A = chi X,the carrier of A by FUNCT_2:18; :: thesis: verum