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 A1, FUNCT_3:def 3; :: thesis: verum