let X be set ; :: thesis: for V being Subset of X holds
( (chi V,X) " {1} = V & (chi V,X) " {0 } = X \ V )
let V be Subset of X; :: thesis: ( (chi V,X) " {1} = V & (chi V,X) " {0 } = X \ V )
thus (chi V,X) " {1} = V :: thesis: (chi V,X) " {0 } = X \ V

proof

thus (chi V,X) " {1} c= V :: according to XBOOLE_0:def 10 :: thesis: V c= (chi V,X) " {1}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (chi V,X) " {1} or x in V )
assume x in (chi V,X) " {1} ; :: thesis: x in V
then ( x in dom (chi V,X) & (chi V,X) . x in {1} ) by FUNCT_1:def 13;
then ( x in X & (chi V,X) . x = 1 ) by TARSKI:def 1;
hence x in V by FUNCT_3:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in V or x in (chi V,X) " {1} )
assume A1: x in V ; :: thesis: x in (chi V,X) " {1}
then x in X ;
then A2: x in dom (chi V,X) by FUNCT_3:def 3;
(chi V,X) . x = 1 by A1, FUNCT_3:def 3;
then (chi V,X) . x in {1} by TARSKI:def 1;
hence x in (chi V,X) " {1} by A2, FUNCT_1:def 13; :: thesis: verum

end;

thus (chi V,X) " {0 } = X \ V :: thesis: verum

proof

thus (chi V,X) " {0 } c= X \ V :: according to XBOOLE_0:def 10 :: thesis: X \ V c= (chi V,X) " {0 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (chi V,X) " {0 } or x in X \ V )
assume A3: x in (chi V,X) " {0 } ; :: thesis: x in X \ V
then A4: ( x in dom (chi V,X) & (chi V,X) . x in {0 } ) by FUNCT_1:def 13;
( ( x in V implies (chi V,X) . x = 1 ) & ( not x in V implies (chi V,X) . x = 0 ) ) by A3, FUNCT_3:def 3;
hence x in X \ V by A4, TARSKI:def 1, XBOOLE_0:def 5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ V or x in (chi V,X) " {0 } )
assume x in X \ V ; :: thesis: x in (chi V,X) " {0 }
then ( x in X & not x in V ) by XBOOLE_0:def 5;
then ( x in dom (chi V,X) & (chi V,X) . x = 0 ) by FUNCT_3:def 3;
then ( x in dom (chi V,X) & (chi V,X) . x in {0 } ) by TARSKI:def 1;
hence x in (chi V,X) " {0 } by FUNCT_1:def 13; :: thesis: verum

end;