thus ( f is constant implies ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d ) :: thesis: ( ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d implies f is constant )

proof

assume Z: f is constant ; :: thesis: ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d

per cases ( dom f = {} or dom f <> {} ) ;

suppose S: dom f = {} ; :: thesis: ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d

consider d being Element of D;
take d ; :: thesis: for c being Element of C st c in dom f holds
f . c = d
thus for c being Element of C st c in dom f holds
f . c = d by S; :: thesis: verum

end;

suppose dom f <> {} ; :: thesis: ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d

then consider c0 being set such that
W: c0 in dom f by XBOOLE_0:def 1;
reconsider c0 = c0 as Element of C by W;
take d = f /. c0; :: thesis: for c being Element of C st c in dom f holds
f . c = d
let c be Element of C; :: thesis: ( c in dom f implies f . c = d )
assume c in dom f ; :: thesis: f . c = d
hence f . c = f . c0 by W, Z, FUNCT_1:def 16
.= d by W, PARTFUN1:def 8 ;
:: thesis: verum

end;

end;

end;

given d being Element of D such that G1: for c being Element of C st c in dom f holds
f . c = d ; :: thesis: f is constant
let x, y be set ; :: according to FUNCT_1:def 16 :: thesis: ( not x in dom f or not y in dom f or f . x = f . y )
assume that
Z1: x in dom f and
Z2: y in dom f ; :: thesis: f . x = f . y
thus f . x = d by Z1, G1
.= f . y by Z2, G1 ; :: thesis: verum