let n be Nat; :: thesis: for X being Subspace of RealVectSpace (Seg n)
for x being Element of REAL n
for a being Real st x in the carrier of X holds
a * x in the carrier of X
let X be Subspace of RealVectSpace (Seg n); :: thesis: for x being Element of REAL n
for a being Real st x in the carrier of X holds
a * x in the carrier of X
let x be Element of REAL n; :: thesis: for a being Real st x in the carrier of X holds
a * x in the carrier of X
let a be Real; :: thesis: ( x in the carrier of X implies a * x in the carrier of X )
reconsider x1 = x as Element of (RealVectSpace (Seg n)) by FINSEQ_2:93;
assume x in the carrier of X ; :: thesis: a * x in the carrier of X
then A1: x in X ;
reconsider aa = a as Element of REAL by XREAL_0:def 1;
aa * x = aa * x1 ;
then a * x in X by A1, RLSUB_1:21;
hence a * x in the carrier of X ; :: thesis: verum