let A be non empty set ; :: thesis: (chi (A,A)) | A is constant
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
for x being Element of A st x in A /\ (dom (chi (A,A))) holds
(chi (A,A)) /. x = jj

proof

let x be Element of A; :: thesis: ( x in A /\ (dom (chi (A,A))) implies (chi (A,A)) /. x = jj )
assume x in A /\ (dom (chi (A,A))) ; :: thesis: (chi (A,A)) /. x = jj
then A1: x in dom (chi (A,A)) by XBOOLE_0:def 4;
(chi (A,A)) . x = 1 by FUNCT_3:def 3;
hence (chi (A,A)) /. x = jj by A1, PARTFUN1:def 6; :: thesis: verum

end;

hence (chi (A,A)) | A is constant by PARTFUN2:35; :: thesis: verum