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 Th18;
dom (chi (A,A)) = A by FUNCT_3:def 3;
then A2: A = A /\ (dom (chi (A,A))) ;
then A3: A = dom ((chi (A,A)) | A) by RELAT_1:61;
A4: A = dom (chi (A,A)) by FUNCT_3:def 3;
for x being Element of A st x in A holds
(chi (A,A)) . x = ((chi (A,A)) | A) . x

proof

let x be Element of A; :: thesis: ( x in A implies (chi (A,A)) . x = ((chi (A,A)) | A) . x )
assume x in A ; :: thesis: (chi (A,A)) . x = ((chi (A,A)) | A) . x
A5: (chi (A,A)) /. x = (chi (A,A)) . x by A4, PARTFUN1:def 6;
(chi (A,A)) /. x = ((chi (A,A)) | A) /. x by A3, PARTFUN2:15;
hence (chi (A,A)) . x = ((chi (A,A)) | A) . x by A3, A5, PARTFUN1:def 6; :: thesis: verum

end;

then A6: chi (A,A) = (chi (A,A)) | A by A4, A3, PARTFUN1:5;
A7: 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
A8: x in dom (chi (A,A)) by A7, 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 A8, FUNCT_3:def 3; :: thesis: verum

end;

then A9: 1 in rng (chi (A,A)) by FUNCT_1:def 3;
A meets dom (chi (A,A)) by A2, XBOOLE_0:def 7;
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 A6, A9, TARSKI:def 1; :: thesis: verum