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 that
A1: x in the carrier of X and
A2: y in the carrier of X ; :: thesis: x + y in the carrier of X
A3: y in X by A2;
reconsider x1 = x, y1 = y as Element of (RealVectSpace (Seg n)) by FINSEQ_2:93;
A4: x1 + y1 = x + y ;
x in X by A1;
then x + y in X by A3, A4, RLSUB_1:20;
hence x + y in the carrier of X ; :: thesis: verum