let F be Function; :: thesis: for x, y being object st x in dom F holds
y in rng (F +* (x,y))
let x, y be object ; :: 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 Th29, Th30;
hence y in rng (F +* (x,y)) by FUNCT_1:3; :: thesis: verum