let n be Nat; :: thesis: for X being Subspace of RealVectSpace (Seg n)
for x, y being Element of REAL n st x in the carrier of X & y in the carrier of X holds
x + y in the carrier of X
let X be Subspace of RealVectSpace (Seg n); :: thesis: for x, y being Element of REAL n st x in the carrier of X & y in the carrier of X holds
x + y in the carrier of X
let x, y be Element of REAL n; :: thesis: ( x in the carrier of X & y in the carrier of X implies x + y in the carrier of X )
assume ( x in the carrier of X & y in the carrier of X ) ; :: thesis: x + y in the carrier of X
then A1: ( x in X & y in X ) by STRUCT_0:def 5;
reconsider x1 = x, y1 = y as Element of (RealVectSpace (Seg n)) by FINSEQ_2:111;
x1 + y1 = x + y ;
then x + y in X by A1, RLSUB_1:28;
hence x + y in the carrier of X by STRUCT_0:def 5; :: thesis: verum