let a, b be Real; :: thesis: for A being closed-interval Subset of REAL holds chi A,A = (Cst 1) | A
let A be closed-interval Subset of REAL ; :: thesis: chi A,A = (Cst 1) | A
( dom ((Cst 1) | A) = A & ( for x being set st x in A holds
( ( x in A implies ((Cst 1) | A) . x = 1 ) & ( not x in A implies ((Cst 1) | A) . x = 0 ) ) ) )

proof

A1: dom (Cst 1) = REAL by FUNCOP_1:19;
A2: dom ((Cst 1) | A) = (dom (Cst 1)) /\ A by RELAT_1:90;
hence dom ((Cst 1) | A) = A by A1, XBOOLE_1:28; :: thesis: for x being set st x in A holds
( ( x in A implies ((Cst 1) | A) . x = 1 ) & ( not x in A implies ((Cst 1) | A) . x = 0 ) )
let x be set ; :: thesis: ( x in A implies ( ( x in A implies ((Cst 1) | A) . x = 1 ) & ( not x in A implies ((Cst 1) | A) . x = 0 ) ) )
assume A3: x in A ; :: thesis: ( ( x in A implies ((Cst 1) | A) . x = 1 ) & ( not x in A implies ((Cst 1) | A) . x = 0 ) )
then x in dom ((Cst 1) | A) by A1, A2, XBOOLE_0:def 4;
then ((Cst 1) | A) . x = (REAL --> 1) . x by FUNCT_1:70
.= 1 by A3, FUNCOP_1:13 ;
hence ( ( x in A implies ((Cst 1) | A) . x = 1 ) & ( not x in A implies ((Cst 1) | A) . x = 0 ) ) by A3; :: thesis: verum

end;

hence chi A,A = (Cst 1) | A by FUNCT_3:def 3; :: thesis: verum