let f be Function; :: thesis: for x, y being set st x in rng f holds
y in rng (f +~ x,y)
let x, y be set ; :: thesis: ( x in rng f implies y in rng (f +~ x,y) )
assume x in rng f ; :: thesis: y in rng (f +~ x,y)
then consider z being set such that
W1: z in dom f and
W2: f . z = x by FUNCT_1:def 5;
x in dom (x .--> y) by FUNCOP_1:89;
then A: z in dom ((x .--> y) * f) by W1, W2, FUNCT_1:21;
B: dom ((x .--> y) * f) c= dom (f +~ x,y) by Th11;
(f +~ x,y) . z = ((x .--> y) * f) . z by Th14, A
.= (x .--> y) . (f . z) by W1, FUNCT_1:23
.= y by W2, FUNCOP_1:87 ;
hence y in rng (f +~ x,y) by A, B, FUNCT_1:12; :: thesis: verum