let X be non empty set ; :: thesis: for A being non empty Subset of X holds rng (chi (A,A)) = {1}
let A be non empty Subset of X; :: thesis: rng (chi (A,A)) = {1}
A1: (chi (A,A)) | A is constant by Th14;
dom (chi (A,A)) = A by FUNCT_3:def 3;
then A2: A = A /\ (dom (chi (A,A))) ;
A3: dom (chi (A,A)) = A by FUNCT_3:def 3;
ex x being Element of X st
( x in dom (chi (A,A)) & (chi (A,A)) . x = 1 )

proof

consider x being Element of X such that
A4: x in dom (chi (A,A)) by A3, SUBSET_1:4;
take x ; :: thesis: ( x in dom (chi (A,A)) & (chi (A,A)) . x = 1 )
thus ( x in dom (chi (A,A)) & (chi (A,A)) . x = 1 ) by A4, FUNCT_3:def 3; :: thesis: verum

end;

then A5: 1 in rng (chi (A,A)) by FUNCT_1:def 3;
A meets dom (chi (A,A)) by A2;
then ex y being Element of REAL st rng ((chi (A,A)) | A) = {y} by A1, PARTFUN2:37;
hence rng (chi (A,A)) = {1} by A5, TARSKI:def 1; :: thesis: verum