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 that
A1: c in dom f and
A2: c in X ; :: thesis: f /. c in rng (f | X)
f . c in rng (f | X) by A1, A2, FUNCT_1:50;
hence f /. c in rng (f | X) by A1, PARTFUN1:def 6; :: thesis: verum