let a, b be Real; :: thesis: for A being non empty closed_interval Subset of REAL holds chi (A,A) = (Cst 1) | A
let A be non empty closed_interval Subset of REAL; :: thesis: chi (A,A) = (Cst 1) | A
( dom ((Cst 1) | A) = A & ( for x being object 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 & dom ((Cst 1) | A) = (dom (Cst 1)) /\ A ) by FUNCOP_1:13, RELAT_1:61;
hence dom ((Cst 1) | A) = A by XBOOLE_1:28; :: thesis: for x being object 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 object ; :: 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 A2: 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, XBOOLE_0:def 4;
then ((Cst 1) | A) . x = (REAL --> 1) . x by FUNCT_1:47
.= 1 by A2, FUNCOP_1:7 ;
hence ( ( x in A implies ((Cst 1) | A) . x = 1 ) & ( not x in A implies ((Cst 1) | A) . x = 0 ) ) by A2; :: thesis: verum

end;

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