let C, D be non empty set ; :: thesis: for SC being Subset of C
for d being Element of D holds (SC --> d) | SC is constant
let SC be Subset of C; :: thesis: for d being Element of D holds (SC --> d) | SC is constant
let d be Element of D; :: thesis: (SC --> d) | SC is constant
take d ; :: according to PARTFUN2:def 1 :: thesis: for c being Element of C st c in dom ((SC --> d) | SC) holds
((SC --> d) | SC) . c = d
let c be Element of C; :: thesis: ( c in dom ((SC --> d) | SC) implies ((SC --> d) | SC) . c = d )
assume A1: c in dom ((SC --> d) | SC) ; :: thesis: ((SC --> d) | SC) . c = d
then A2: c in SC /\ (dom (SC --> d)) by RELAT_1:61;
then c in SC by XBOOLE_0:def 4;
then (SC --> d) /. c = d by Th29;
then ((SC --> d) | SC) /. c = d by A2, Th16;
hence ((SC --> d) | SC) . c = d by A1, PARTFUN1:def 6; :: thesis: verum