let C, D be non empty set ; :: thesis: for SC being Subset of C
for d being Element of D
for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds
f | SC is constant
let SC be Subset of C; :: thesis: for d being Element of D
for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds
f | SC is constant
let d be Element of D; :: thesis: for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds
f | SC is constant
let f be PartFunc of C,D; :: thesis: ( f | SC = (dom (f | SC)) --> d implies f | SC is constant )
assume A1: f | SC = (dom (f | SC)) --> d ; :: thesis: f | SC is constant

now :: thesis: for c being Element of C st c in SC /\ (dom f) holds
f /. c = d

let c be Element of C; :: thesis: ( c in SC /\ (dom f) implies f /. c = d )
assume c in SC /\ (dom f) ; :: thesis: f /. c = d
then A2: c in dom (f | SC) by RELAT_1:61;
then (f | SC) /. c = d by A1, Th29;
hence f /. c = d by A2, Th15; :: thesis: verum

end;

hence f | SC is constant by Th35; :: thesis: verum