let X be set ; :: thesis: for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in dom f & c in X holds
f /. c in rng (f | X)
let C, D be non empty set ; :: thesis: for c being Element of C
for f being PartFunc of C,D st c in dom f & c in X holds
f /. c in rng (f | X)
let c be Element of C; :: thesis: for f being PartFunc of C,D st c in dom f & c in X holds
f /. c in rng (f | X)
let f be PartFunc of C,D; :: thesis: ( c in dom f & c in X implies f /. c in rng (f | X) )
assume A1: ( c in dom f & c in X ) ; :: thesis: f /. c in rng (f | X)
then f . c in rng (f | X) by FUNCT_1:73;
hence f /. c in rng (f | X) by A1, PARTFUN1:def 8; :: thesis: verum