let f be Function; :: thesis: for x, y being object st x in rng f holds
y in rng (f +~ (x,y))
let x, y be object ; :: 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 object such that
A1: z in dom f and
A2: f . z = x by FUNCT_1:def 3;
A3: dom ((x .--> y) * f) c= dom (f +~ (x,y)) by Th10;
x in dom (x .--> y) by FUNCOP_1:74;
then A4: z in dom ((x .--> y) * f) by A1, A2, FUNCT_1:11;
then (f +~ (x,y)) . z = ((x .--> y) * f) . z by Th13
.= (x .--> y) . (f . z) by A1, FUNCT_1:13
.= y by A2, FUNCOP_1:72 ;
hence y in rng (f +~ (x,y)) by A4, A3, FUNCT_1:3; :: thesis: verum