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))

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

hence
RAT_Sums (rng x) is Subset of the carrier of (NLin (rng x))
by TARSKI:def 3; :: thesis: verum
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;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