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 A1: ( 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 ) ) ) ) ; :: thesis: f = chi X,C
then for x being set st x in C holds
( ( x in X implies f . x = 1 ) & ( not x in X implies f . x = 0 ) ) ;
hence f = chi X,C by A1, FUNCT_3:def 3; :: thesis: verum