let X be set ; :: thesis: for D, C 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 D, C 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 )

hereby :: 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 )

assume f | X is constant ; :: thesis: ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f . c = d
then consider d being Element of D such that
A1: for c being Element of C st c in X /\ (dom f) holds
f /. c = d by Th54;
take d = 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 c in dom f by XBOOLE_0:def 4;
hence f . c = f /. c by PARTFUN1:def 8
.= d by A1, A2 ;
:: thesis: verum

end;

given d being Element of D such that A3: 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 A4: c in dom (f | X) ; :: thesis: (f | X) . c = d
then A5: c in X /\ (dom f) by RELAT_1:90;
then A6: c in dom f by XBOOLE_0:def 4;
thus (f | X) . c = (f | X) /. c by A4, PARTFUN1:def 8
.= f /. c by A5, Th34
.= f . c by A6, PARTFUN1:def 8
.= d by A3, A5 ; :: thesis: verum