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);
{(In (0,REAL)),(In (1,REAL))} c= REAL ;
then reconsider G = chi (X, the carrier of A) as Function of the carrier of A,REAL by FUNCT_2:7;
for x being object st x in the carrier of A holds
F . x = G . x

proof

let x be object ; :: 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:12; :: thesis: verum