let X be set ; for V being Subset of X holds
( (chi (V,X)) " {1} = V & (chi (V,X)) " {0} = X \ V )
let V be Subset of X; ( (chi (V,X)) " {1} = V & (chi (V,X)) " {0} = X \ V )
thus
(chi (V,X)) " {1} = V
(chi (V,X)) " {0} = X \ V
thus
(chi (V,X)) " {0} = X \ V
verumproof
thus
(chi (V,X)) " {0} c= X \ V
XBOOLE_0:def 10 X \ V c= (chi (V,X)) " {0}
let x be
object ;
TARSKI:def 3 ( not x in X \ V or x in (chi (V,X)) " {0} )
assume A6:
x in X \ V
;
x in (chi (V,X)) " {0}
then
not
x in V
by XBOOLE_0:def 5;
then
(chi (V,X)) . x = 0
by A6, FUNCT_3:def 3;
then A7:
(chi (V,X)) . x in {0}
by TARSKI:def 1;
x in X
by A6;
then
x in dom (chi (V,X))
by FUNCT_3:def 3;
hence
x in (chi (V,X)) " {0}
by A7, FUNCT_1:def 7;
verum
end;