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 A & 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 8; :: thesis: verum

end;

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