let X be RealNormSpace; :: thesis: for x being sequence of X holds RAT_Sums (rng x) is Subset of the carrier of (NLin (rng x))
let x be sequence of X; :: thesis: RAT_Sums (rng x) is Subset of the carrier of (NLin (rng x))
set D = RAT_Sums (rng x);
for z being object st z in RAT_Sums (rng x) holds
z in the carrier of (NLin (rng x))
proof
let z be object ; :: thesis: ( z in RAT_Sums (rng x) implies z in the carrier of (NLin (rng x)) )
assume z in RAT_Sums (rng x) ; :: thesis: z in the carrier of (NLin (rng x))
then consider l being Linear_Combination of rng x such that
A2: ( z = Sum l & rng l c= RAT ) ;
z in Lin (rng x) by A2, RLVECT_3:14;
hence z in the carrier of (NLin (rng x)) ; :: thesis: verum
end;
hence RAT_Sums (rng x) is Subset of the carrier of (NLin (rng x)) by TARSKI:def 3; :: thesis: verum