let X be set ; :: thesis: for A being Subset of X holds ((0,1) --> (1,0)) * (chi (A,X)) = chi ((A `),X)

let A be Subset of X; :: thesis: ((0,1) --> (1,0)) * (chi (A,X)) = chi ((A `),X)

set f = ((0,1) --> (1,0)) * (chi (A,X));

A1: dom (chi (A,X)) = X by FUNCT_3:def 3;

A2: for x being object st x in X holds

( ( x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 ) & ( not x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 ) )

then rng (chi (A,X)) c= dom ((0,1) --> (1,0)) by FUNCT_3:39;

hence ((0,1) --> (1,0)) * (chi (A,X)) = chi ((A `),X) by A2, FUNCT_3:def 3, A1, RELAT_1:27; :: thesis: verum

let A be Subset of X; :: thesis: ((0,1) --> (1,0)) * (chi (A,X)) = chi ((A `),X)

set f = ((0,1) --> (1,0)) * (chi (A,X));

A1: dom (chi (A,X)) = X by FUNCT_3:def 3;

A2: for x being object st x in X holds

( ( x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 ) & ( not x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 ) )

proof

dom ((0,1) --> (1,0)) = {0,1}
by FUNCT_4:62;
let x be object ; :: thesis: ( x in X implies ( ( x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 ) & ( not x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 ) ) )

assume A3: x in X ; :: thesis: ( ( x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 ) & ( not x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 ) )

thus ( x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 ) :: thesis: ( not x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 )

then x in A by A3, XBOOLE_0:def 5;

then (chi (A,X)) . x = 1 by FUNCT_3:def 3;

then (((0,1) --> (1,0)) * (chi (A,X))) . x = ((0,1) --> (1,0)) . 1 by A1, A3, FUNCT_1:13;

hence (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 by FUNCT_4:63; :: thesis: verum

end;assume A3: x in X ; :: thesis: ( ( x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 ) & ( not x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 ) )

thus ( x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 ) :: thesis: ( not x in A ` implies (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 )

proof

assume
not x in A `
; :: thesis: (((0,1) --> (1,0)) * (chi (A,X))) . x = 0
assume
x in A `
; :: thesis: (((0,1) --> (1,0)) * (chi (A,X))) . x = 1

then not x in A by XBOOLE_0:def 5;

then (chi (A,X)) . x = 0 by A3, FUNCT_3:def 3;

then (((0,1) --> (1,0)) * (chi (A,X))) . x = ((0,1) --> (1,0)) . 0 by A1, A3, FUNCT_1:13;

hence (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 by FUNCT_4:63; :: thesis: verum

end;then not x in A by XBOOLE_0:def 5;

then (chi (A,X)) . x = 0 by A3, FUNCT_3:def 3;

then (((0,1) --> (1,0)) * (chi (A,X))) . x = ((0,1) --> (1,0)) . 0 by A1, A3, FUNCT_1:13;

hence (((0,1) --> (1,0)) * (chi (A,X))) . x = 1 by FUNCT_4:63; :: thesis: verum

then x in A by A3, XBOOLE_0:def 5;

then (chi (A,X)) . x = 1 by FUNCT_3:def 3;

then (((0,1) --> (1,0)) * (chi (A,X))) . x = ((0,1) --> (1,0)) . 1 by A1, A3, FUNCT_1:13;

hence (((0,1) --> (1,0)) * (chi (A,X))) . x = 0 by FUNCT_4:63; :: thesis: verum

then rng (chi (A,X)) c= dom ((0,1) --> (1,0)) by FUNCT_3:39;

hence ((0,1) --> (1,0)) * (chi (A,X)) = chi ((A `),X) by A2, FUNCT_3:def 3, A1, RELAT_1:27; :: thesis: verum