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

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