let X be set ; :: thesis: for C, D being non empty set
for f being PartFunc of C,D holds
( f | X is constant iff ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d )
let C, D be non empty set ; :: thesis: for f being PartFunc of C,D holds
( f | X is constant iff ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d )
let f be PartFunc of C,D; :: thesis: ( f | X is constant iff ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d )
thus ( f | X is constant implies ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d ) :: thesis: ( ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d implies f | X is constant )

proof

given d being Element of D such that A1: for c being Element of C st c in dom (f | X) holds
(f | X) . c = d ; :: according to PARTFUN2:def 1 :: thesis: ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d
take d ; :: thesis: for c being Element of C st c in X /\ (dom f) holds
f /. c = d
let c be Element of C; :: thesis: ( c in X /\ (dom f) implies f /. c = d )
assume A2: c in X /\ (dom f) ; :: thesis: f /. c = d
then A3: c in dom (f | X) by RELAT_1:61;
c in dom f by A2, XBOOLE_0:def 4;
hence f /. c = f . c by PARTFUN1:def 6
.= (f | X) . c by A3, FUNCT_1:47
.= d by A1, A3 ;
:: thesis: verum

end;

given d being Element of D such that A4: for c being Element of C st c in X /\ (dom f) holds
f /. c = d ; :: thesis: f | X is constant
take d ; :: according to PARTFUN2:def 1 :: thesis: for c being Element of C st c in dom (f | X) holds
(f | X) . c = d
let c be Element of C; :: thesis: ( c in dom (f | X) implies (f | X) . c = d )
assume A5: c in dom (f | X) ; :: thesis: (f | X) . c = d
then A6: c in X /\ (dom f) by RELAT_1:61;
then A7: c in dom f by XBOOLE_0:def 4;
thus (f | X) . c = f . c by A5, FUNCT_1:47
.= f /. c by A7, PARTFUN1:def 6
.= d by A4, A6 ; :: thesis: verum