let V be RealLinearSpace; :: thesis: rng (ZeroLC V) c= INT
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (ZeroLC V) or y in INT )
assume AD: y in rng (ZeroLC V) ; :: thesis: y in INT
consider x being set such that
R1: ( x in the carrier of V & y = (ZeroLC V) . x ) by AD, FUNCT_2:17;
reconsider z = x as VECTOR of V by R1;
(ZeroLC V) . z = 0 by RLVECT_2:30;
hence y in INT by R1, NUMBERS:17, TARSKI:def 3; :: thesis: verum