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 = r (#) (chi A,A) implies ( f is total & rng f = {r} ) )

proof

assume A2: f = r (#) (chi A,A) ; :: thesis: ( f is total & rng f = {r} )
A3: chi A,A is total by RFUNCT_1:78;
hence f is total by A2; :: thesis: rng f = {r}
A4: dom f = A by A2, A3, PARTFUN1:def 4;
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 A5: x = r by TARSKI:def 1;
consider a being Real such that
A6: a in dom f by A4, SUBSET_1:10;
(chi A,A) . a = 1 by A6, RFUNCT_1:79;
then f . a = r * 1 by A2, A6, VALUED_1:def 5;
hence x in rng f by A5, A6, FUNCT_1:def 5; :: thesis: verum

end;

then A7: {r} c= rng f by TARSKI:def 3;
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
A8: a in dom f and
A9: f . a = x by PARTFUN1:26;
(chi A,A) . a = 1 by RFUNCT_1:79;
then x = r * 1 by A2, A8, A9, VALUED_1:def 5
.= r ;
hence x in {r} by TARSKI:def 1; :: thesis: verum

end;

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

end;

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

proof

reconsider g = r (#) (chi A,A) as PartFunc of A,REAL ;
assume A10: f is total ; :: thesis: ( not rng f = {r} or f = r (#) (chi A,A) )
A11: chi A,A is total by RFUNCT_1:78;
A12: dom g = dom (chi A,A) by VALUED_1:def 5
.= A by A11, PARTFUN1:def 4 ;
assume A13: rng f = {r} ; :: thesis: f = r (#) (chi A,A)
A14: 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 A15: x in dom f ; :: thesis: f /. x = g /. x
then f /. x = f . x by PARTFUN1:def 8;
then A16: f /. x in rng f by A15, FUNCT_1:def 5;
g /. x = g . x by A12, PARTFUN1:def 8
.= r * ((chi A,A) . x) by A12, VALUED_1:def 5
.= r * 1 by RFUNCT_1:79
.= r ;
hence f /. x = g /. x by A13, A16, TARSKI:def 1; :: thesis: verum

end;

dom f = dom g by A10, A12, PARTFUN1:def 4;
hence f = r (#) (chi A,A) by A14, PARTFUN2:3; :: thesis: verum

end;

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