let X be non empty set ; for A being non empty Subset of X holds rng (chi A,A) = {1}
let A be non empty Subset of X; 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:90;
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;
( x in A implies (chi A,A) . x = ((chi A,A) | A) . x )
assume
x in A
;
(chi A,A) . x = ((chi A,A) | A) . x
A5:
(chi A,A) /. x = (chi A,A) . x
by A4, PARTFUN1:def 8;
(chi A,A) /. x = ((chi A,A) | A) /. x
by A3, PARTFUN2:32;
hence
(chi A,A) . x = ((chi A,A) | A) . x
by A3, A5, PARTFUN1:def 8;
verum
end;
then A6:
chi A,A = (chi A,A) | A
by A4, A3, PARTFUN1:34;
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 )
then A9:
1 in rng (chi A,A)
by FUNCT_1:def 5;
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:56;
hence
rng (chi A,A) = {1}
by A6, A9, TARSKI:def 1; verum