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 ) )
proof
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 )
proof
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;
assume not x in A ` ; :: thesis: (((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;
dom ((0,1) --> (1,0)) = {0,1} by FUNCT_4:62;
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