let X, Y be set ; :: thesis: for C, D being non empty set
for f being PartFunc of C,D st f | X is constant & Y c= X holds
f | Y is constant
let C, D be non empty set ; :: thesis: for f being PartFunc of C,D st f | X is constant & Y c= X holds
f | Y is constant
let f be PartFunc of C,D; :: thesis: ( f | X is constant & Y c= X implies f | Y is constant )
assume A1: ( f | X is constant & Y c= X ) ; :: thesis: f | Y is constant
then consider d being Element of D such that
A2: for c being Element of C st c in X /\ (dom f) holds
f /. c = d by Thx;

now

let c be Element of C; :: thesis: ( c in Y /\ (dom f) implies f /. c = d )
assume c in Y /\ (dom f) ; :: thesis: f /. c = d
then ( c in Y & c in dom f ) by XBOOLE_0:def 4;
then c in X /\ (dom f) by A1, XBOOLE_0:def 4;
hence f /. c = d by A2; :: thesis: verum

end;

hence f | Y is constant by Thx; :: thesis: verum