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
A1: z in dom f and
A2: f . z = x by FUNCT_1:def 5;
A3: dom ((x .--> y) * f) c= dom (f +~ (x,y)) by Th11;
x in dom (x .--> y) by FUNCOP_1:89;
then A4: z in dom ((x .--> y) * f) by A1, A2, FUNCT_1:21;
then (f +~ (x,y)) . z = ((x .--> y) * f) . z by Th14
.= (x .--> y) . (f . z) by A1, FUNCT_1:23
.= y by A2, FUNCOP_1:87 ;
hence y in rng (f +~ (x,y)) by A4, A3, FUNCT_1:12; :: thesis: verum