let n be Nat; :: thesis: for X being Subspace of RealVectSpace (Seg n)
for x, y being Element of REAL n
for a, b being Real st x in the carrier of X & y in the carrier of X holds
(a * x) + (b * y) in the carrier of X
let X be Subspace of RealVectSpace (Seg n); :: thesis: for x, y being Element of REAL n
for a, b being Real st x in the carrier of X & y in the carrier of X holds
(a * x) + (b * y) in the carrier of X
let x, y be Element of REAL n; :: thesis: for a, b being Real st x in the carrier of X & y in the carrier of X holds
(a * x) + (b * y) in the carrier of X
let a, b be Real; :: thesis: ( x in the carrier of X & y in the carrier of X implies (a * x) + (b * y) in the carrier of X )
assume that
A1: x in the carrier of X and
A2: y in the carrier of X ; :: thesis: (a * x) + (b * y) in the carrier of X
A3: b * y in the carrier of X by A2, Th34;
a * x in the carrier of X by A1, Th34;
hence (a * x) + (b * y) in the carrier of X by A3, Th35; :: thesis: verum