let x, y be set ; :: thesis: rng (x .--> y) = {y}
dom (x .--> y) = {x} ;
hence rng (x .--> y) = {((x .--> y) . x)} by FUNCT_1:4
.= {y} by Th72 ;
:: thesis: verum