let x be set ; :: thesis: for C, D being non empty set
for f being PartFunc of C,D holds f | {x} is constant
let C, D be non empty set ; :: thesis: for f being PartFunc of C,D holds f | {x} is constant
let f be PartFunc of C,D; :: thesis: f | {x} is constant

now :: thesis: f | {x} is constant

per cases ( {x} /\ (dom f) = {} or {x} /\ (dom f) <> {} ) ;

suppose {x} /\ (dom f) = {} ; :: thesis: f | {x} is constant

then {x} misses dom f ;
hence f | {x} is constant by Th39; :: thesis: verum

end;

suppose A1: {x} /\ (dom f) <> {} ; :: thesis: f | {x} is constant

set y = the Element of {x} /\ (dom f);
( the Element of {x} /\ (dom f) in {x} & the Element of {x} /\ (dom f) in dom f ) by A1, XBOOLE_0:def 4;
then reconsider x1 = x as Element of C by TARSKI:def 1;

now :: thesis: ex d being Element of D st
for c being Element of C st c in {x} /\ (dom f) holds
f /. c = f /. x1

take d = f /. x1; :: thesis: for c being Element of C st c in {x} /\ (dom f) holds
f /. c = f /. x1
let c be Element of C; :: thesis: ( c in {x} /\ (dom f) implies f /. c = f /. x1 )
assume c in {x} /\ (dom f) ; :: thesis: f /. c = f /. x1
then c in {x} by XBOOLE_0:def 4;
hence f /. c = f /. x1 by TARSKI:def 1; :: thesis: verum

end;

hence f | {x} is constant by Th35; :: thesis: verum

end;

end;

end;

hence f | {x} is constant ; :: thesis: verum