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 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
per cases ( dom f = {} or dom f <> {} ) ;
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
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;
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 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;
end;
end;
given d being Element of D such that A4: for c being Element of C st c in dom f holds
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