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 Thx;
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 Z: c in dom (f | X) ; :: thesis: (f | X) . c = d
then A4: c in X /\ (dom f) by RELAT_1:90;
then B4: c in dom f by XBOOLE_0:def 4;
thus (f | X) . c = (f | X) /. c by Z, PARTFUN1:def 8
.= f /. c by A4, Th34
.= f . c by B4, PARTFUN1:def 8
.= d by A3, A4 ; :: thesis: verum