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 )

f . c = d ; :: thesis: f is constant

let x, y be object ; :: according to FUNCT_1:def 10 :: thesis: ( not x in dom f or not y in dom f or f . x = f . y )

assume that

A5: x in dom f and

A6: y in dom f ; :: thesis: f . x = f . y

thus f . x = d by A4, A5

.= f . y by A4, A6 ; :: thesis: verum

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

given d being Element of D such that A4:
for c being Element of C st c in dom f holds
assume A1:
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

end;for c being Element of C st c in dom f holds

f . c = d

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

end;

suppose A2:
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

for c being Element of C st c in dom f holds

f . c = d

set d = the Element of D;

take the Element of D ; :: thesis: for c being Element of C st c in dom f holds

f . c = the Element of D

thus for c being Element of C st c in dom f holds

f . c = the Element of D by A2; :: thesis: verum

end;take the Element of D ; :: thesis: for c being Element of C st c in dom f holds

f . c = the Element of D

thus for c being Element of C st c in dom f holds

f . c = the Element of D by A2; :: thesis: verum

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

for c being Element of C st c in dom f holds

f . c = d

then consider c0 being object such that

A3: c0 in dom f by XBOOLE_0:def 1;

reconsider c0 = c0 as Element of C by A3;

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 A1, A3

.= d by A3, PARTFUN1:def 6 ;

:: thesis: verum

end;A3: c0 in dom f by XBOOLE_0:def 1;

reconsider c0 = c0 as Element of C by A3;

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 A1, A3

.= d by A3, PARTFUN1:def 6 ;

:: thesis: verum

f . c = d ; :: thesis: f is constant

let x, y be object ; :: according to FUNCT_1:def 10 :: thesis: ( not x in dom f or not y in dom f or f . x = f . y )

assume that

A5: x in dom f and

A6: y in dom f ; :: thesis: f . x = f . y

thus f . x = d by A4, A5

.= f . y by A4, A6 ; :: thesis: verum