let X be set ; :: thesis: for C being non empty set
for f being PartFunc of C,REAL holds
( f = chi (X,C) iff ( dom f = C & ( for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) )

let C be non empty set ; :: thesis: for f being PartFunc of C,REAL holds
( f = chi (X,C) iff ( dom f = C & ( for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) )

let f be PartFunc of C,REAL; :: thesis: ( f = chi (X,C) iff ( dom f = C & ( for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) )

thus ( f = chi (X,C) implies ( dom f = C & ( for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) ) by FUNCT_3:def 3; :: thesis: ( dom f = C & ( for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) implies f = chi (X,C) )

assume that
A1: dom f = C and
A2: for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ; :: thesis: f = chi (X,C)
for x being object st x in C holds
( ( x in X implies f . x = 1 ) & ( not x in X implies f . x = 0 ) ) by A2;
hence f = chi (X,C) by ; :: thesis: verum