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 set 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 set ; :: 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:23;
hence ((0 ,1 --> 1,0 ) * (chi A,X)) . x = 1 by FUNCT_4:66; :: 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:23;
hence ((0 ,1 --> 1,0 ) * (chi A,X)) . x = 0 by FUNCT_4:66; :: thesis: verum

end;

dom (0 ,1 --> 1,0 ) = {0 ,1} by FUNCT_4:65;
then rng (chi A,X) c= dom (0 ,1 --> 1,0 ) by FUNCT_3:48;
then dom ((0 ,1 --> 1,0 ) * (chi A,X)) = X by A1, RELAT_1:46;
hence (0 ,1 --> 1,0 ) * (chi A,X) = chi (A ` ),X by A2, FUNCT_3:def 3; :: thesis: verum