for o being object st o in rng f holds
o in the carrier of V ;
hence rng f is Subset of V ; :: thesis: verum