let A be closed-interval Subset of REAL ; :: thesis: for f being PartFunc of A,REAL
for r being Real holds
( ( f is total & rng f = {r} ) iff f = r (#) (chi A,A) )
let f be PartFunc of A,REAL ; :: thesis: for r being Real holds
( ( f is total & rng f = {r} ) iff f = r (#) (chi A,A) )
let r be Real; :: thesis: ( ( f is total & rng f = {r} ) iff f = r (#) (chi A,A) )
A1: ( f is total & rng f = {r} implies f = r (#) (chi A,A) )

proof

assume A2: f is total ; :: thesis: ( not rng f = {r} or f = r (#) (chi A,A) )
assume A3: rng f = {r} ; :: thesis: f = r (#) (chi A,A)
reconsider g = r (#) (chi A,A) as PartFunc of A,REAL ;
A4: chi A,A is total by RFUNCT_1:78;
A5: dom g = dom (chi A,A) by VALUED_1:def 5
.= A by A4, PARTFUN1:def 4 ;
then A6: dom f = dom g by A2, PARTFUN1:def 4;
for x being Element of A st x in dom f holds
f /. x = g /. x

proof

let x be Element of A; :: thesis: ( x in dom f implies f /. x = g /. x )
assume A7: x in dom f ; :: thesis: f /. x = g /. x
then f /. x = f . x by PARTFUN1:def 8;
then A8: f /. x in rng f by A7, FUNCT_1:def 5;
g /. x = g . x by A5, PARTFUN1:def 8
.= r * ((chi A,A) . x) by A5, VALUED_1:def 5
.= r * 1 by RFUNCT_1:79
.= r ;
hence f /. x = g /. x by A3, A8, TARSKI:def 1; :: thesis: verum

end;

hence f = r (#) (chi A,A) by A6, PARTFUN2:3; :: thesis: verum

end;

( f = r (#) (chi A,A) implies ( f is total & rng f = {r} ) )

proof

assume A9: f = r (#) (chi A,A) ; :: thesis: ( f is total & rng f = {r} )
then ( dom f = dom (chi A,A) & chi A,A is total ) by RFUNCT_1:78, VALUED_1:def 5;
then A10: dom f = A by PARTFUN1:def 4;
hence f is total by PARTFUN1:def 4; :: thesis: rng f = {r}
for x being set st x in rng f holds
x in {r}

proof

let x be set ; :: thesis: ( x in rng f implies x in {r} )
assume x in rng f ; :: thesis: x in {r}
then consider a being Element of A such that
A11: ( a in dom f & f . a = x ) by PARTFUN1:26;
(chi A,A) . a = 1 by RFUNCT_1:79;
then x = r * 1 by A9, A11, VALUED_1:def 5
.= r ;
hence x in {r} by TARSKI:def 1; :: thesis: verum

end;

then A12: rng f c= {r} by TARSKI:def 3;
for x being set st x in {r} holds
x in rng f

proof

let x be set ; :: thesis: ( x in {r} implies x in rng f )
assume x in {r} ; :: thesis: x in rng f
then A13: x = r by TARSKI:def 1;
consider a being Real such that
A14: a in dom f by A10, SUBSET_1:10;
(chi A,A) . a = 1 by A14, RFUNCT_1:79;
then f . a = r * 1 by A9, A14, VALUED_1:def 5;
hence x in rng f by A13, A14, FUNCT_1:def 5; :: thesis: verum

end;

then {r} c= rng f by TARSKI:def 3;
hence rng f = {r} by A12, XBOOLE_0:def 10; :: thesis: verum

end;

hence ( ( f is total & rng f = {r} ) iff f = r (#) (chi A,A) ) by A1; :: thesis: verum