set A1 = { (Sum l) where l is Linear_Combination of A : rng l c= INT } ;
{ (Sum l) where l is Linear_Combination of A : rng l c= INT } c= the carrier of V

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Sum l) where l is Linear_Combination of A : rng l c= INT } or x in the carrier of V )
assume x in { (Sum l) where l is Linear_Combination of A : rng l c= INT } ; :: thesis: x in the carrier of V
then ex l being Linear_Combination of A st
( x = Sum l & rng l c= INT ) ;
hence x in the carrier of V ; :: thesis: verum

end;

hence { (Sum l) where l is Linear_Combination of A : rng l c= INT } is Subset of V ; :: thesis: verum