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: A = A /\ (dom (chi A,A))

proof

dom (chi A,A) = A by FUNCT_3:def 3;
hence A = A /\ (dom (chi A,A)) ; :: thesis: verum

end;

A2: chi A,A = (chi A,A) | A

proof

A3: ( A = dom (chi A,A) & A = dom ((chi A,A) | A) ) by A1, FUNCT_3:def 3, RELAT_1:90;
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
A4: (chi A,A) /. x = ((chi A,A) | A) /. x by A3, PARTFUN2:32;
(chi A,A) /. x = (chi A,A) . x by A3, PARTFUN1:def 8;
hence (chi A,A) . x = ((chi A,A) | A) . x by A3, A4, PARTFUN1:def 8; :: thesis: verum

end;

hence chi A,A = (chi A,A) | A by A3, PARTFUN1:34; :: thesis: verum

end;

A5: A meets dom (chi A,A) by A1, XBOOLE_0:def 7;
(chi A,A) | A is constant by Th18;
then consider y being Element of REAL such that
A6: rng ((chi A,A) | A) = {y} by A5, PARTFUN2:56;
y = 1

proof

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:10;
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 1 in rng (chi A,A) by FUNCT_1:def 5;
hence y = 1 by A2, A6, TARSKI:def 1; :: thesis: verum

end;

hence rng (chi A,A) = {1} by A2, A6; :: thesis: verum