let Z be non empty set ; :: thesis: for f being Function of Z,REAL holds
( f is constant iff ex r being Real st f = r (#) (chi (Z,Z)) )
let f be Function of Z,REAL; :: thesis: ( f is constant iff ex r being Real st f = r (#) (chi (Z,Z)) )

hereby :: thesis: ( ex r being Real st f = r (#) (chi (Z,Z)) implies f is constant )

assume A1: f is constant ; :: thesis: ex r being Real st f = r (#) (chi (Z,Z))
set y = the Element of rng f;
consider x being object such that
A2: x in dom f and
A3: the Element of rng f = f . x by FUNCT_1:def 3;
reconsider r = the Element of rng f as Real ;
take r = r; :: thesis: f = r (#) (chi (Z,Z))

now :: thesis: ( dom (r (#) (chi (Z,Z))) = dom f & ( for z being object st z in dom f holds
f . z = (r (#) (chi (Z,Z))) . z ) )

thus A3BIS: dom (r (#) (chi (Z,Z))) = dom (chi (Z,Z)) by VALUED_1:def 5
.= Z by FUNCT_3:def 3
.= dom f by PARTFUN1:def 2 ; :: thesis: for z being object st z in dom f holds
f . z = (r (#) (chi (Z,Z))) . z
thus for z being object st z in dom f holds
f . z = (r (#) (chi (Z,Z))) . z :: thesis: verum

proof

let z be object ; :: thesis: ( z in dom f implies f . z = (r (#) (chi (Z,Z))) . z )
assume A4: z in dom f ; :: thesis: f . z = (r (#) (chi (Z,Z))) . z
then (r (#) (chi (Z,Z))) . z = r * ((chi (Z,Z)) . z) by A3BIS, VALUED_1:def 5
.= r * 1 by A4, FUNCT_3:def 3
.= f . z by A3, A1, A4, A2 ;
hence f . z = (r (#) (chi (Z,Z))) . z ; :: thesis: verum

end;

end;

hence f = r (#) (chi (Z,Z)) ; :: thesis: verum

end;

assume ex r being Real st f = r (#) (chi (Z,Z)) ; :: thesis: f is constant
then consider r being Real such that
A5: f = r (#) (chi (Z,Z)) ;
for x, y being object st x in dom f & y in dom f holds
f . x = f . y

proof

let x, y be object ; :: thesis: ( x in dom f & y in dom f implies f . x = f . y )
assume that
A6: x in dom f and
A7: y in dom f ; :: thesis: f . x = f . y
f . x = r * ((chi (Z,Z)) . x) by A5, A6, VALUED_1:def 5
.= r * 1 by A6, FUNCT_3:def 3
.= r * ((chi (Z,Z)) . y) by A7, FUNCT_3:def 3
.= f . y by A5, A7, VALUED_1:def 5 ;
hence f . x = f . y ; :: thesis: verum

end;

hence f is constant ; :: thesis: verum