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

proof

let x be Element of A; :: thesis: ( x in A /\ (dom (chi (A,A))) implies (chi (A,A)) /. x = 1 )
assume x in A /\ (dom (chi (A,A))) ; :: thesis: (chi (A,A)) /. x = 1
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 = 1 by A1, PARTFUN1:def 6; :: thesis: verum

end;

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