let A be non empty 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:62;
hence f is total by A2; :: thesis: rng f = {r}
A4: dom f = A by A2, A3, PARTFUN1:def 2;
for x being object st x in {r} holds
x in rng f
proof
let x be object ; :: 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 Element of REAL such that
A6: a in dom f by A4, SUBSET_1:4;
(chi (A,A)) . a = 1 by A6, RFUNCT_1:63;
then f . a = r * 1 by A2, A6, VALUED_1:def 5;
hence x in rng f by A5, A6, FUNCT_1:def 3; :: thesis: verum
end;
then A7: {r} c= rng f by TARSKI:def 3;
for x being object st x in rng f holds
x in {r}
proof
let x be object ; :: 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:3;
(chi (A,A)) . a = 1 by RFUNCT_1:63;
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:62;
A12: dom g = dom (chi (A,A)) by VALUED_1:def 5
.= A by A11, PARTFUN1:def 2 ;
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 6;
then A16: f /. x in rng f by A15, FUNCT_1:def 3;
g /. x = g . x by A12, PARTFUN1:def 6
.= r * ((chi (A,A)) . x) by A12, VALUED_1:def 5
.= r * 1 by RFUNCT_1:63
.= r ;
hence f /. x = g /. x by A13, A16, TARSKI:def 1; :: thesis: verum
end;
dom f = dom g by A10, A12, PARTFUN1:def 2;
hence f = r (#) (chi (A,A)) by A14, PARTFUN2:1; :: thesis: verum
end;
hence ( ( f is total & rng f = {r} ) iff f = r (#) (chi (A,A)) ) by A1; :: thesis: verum