let F be Function; :: thesis: for x, y being set st x in dom F holds
y in rng (F +* x,y)
let x, y be set ; :: thesis: ( x in dom F implies y in rng (F +* x,y) )
assume x in dom F ; :: thesis: y in rng (F +* x,y)
then ( x in dom (F +* x,y) & (F +* x,y) . x = y ) by Th32, Th33;
hence y in rng (F +* x,y) by FUNCT_1:12; :: thesis: verum