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

assume f | X is constant ; :: thesis:
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;
let c1, c2 be Element of C; :: thesis:
assume ( c1 in X /\ (dom f) & c2 in X /\ (dom f) ) ; :: thesis:
then ( f /. c1 = d & f /. c2 = d ) by A1;
hence f /. c1 = f /. c2 ; :: thesis:

end;

assume A2: for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f /. c1 = f /. c2 ; :: thesis:

per cases ;

suppose A3: X /\ (dom f) = {} ; :: thesis:

consider d being Element of D;
take d = d; :: thesis:
let c be Element of C; :: thesis:
thus ( c in X /\ (dom f) implies f /. c = d ) by A3; :: thesis:

end;

hence f | X is constant by Thx; :: thesis:

end;

suppose A4: X /\ (dom f) <> {} ; :: thesis:

consider x being Element of X /\ (dom f);
x in dom f by A4, XBOOLE_0:def 4;
then reconsider x = x as Element of C ;
for c being Element of C st c in X /\ (dom f) holds
f /. c = f /. x by A2;
hence f | X is constant by Thx; :: thesis:

end;

hence f | X is constant ; :: thesis: