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

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