let n be Nat; :: thesis: for X being Subspace of RealVectSpace (Seg n)
for x, y being Element of REAL n
for a being Real st x in the carrier of X & y in the carrier of X holds
(a * x) + 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 being Real st x in the carrier of X & y in the carrier of X holds
(a * x) + y in the carrier of X
let x, y be Element of REAL n; :: thesis: for a being Real st x in the carrier of X & y in the carrier of X holds
(a * x) + y in the carrier of X
let a be Real; :: thesis: ( x in the carrier of X & y in the carrier of X implies (a * 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: (a * x) + y in the carrier of X
a * x in the carrier of X by A1, Th34;
hence (a * x) + y in the carrier of X by A2, Th35; :: thesis: verum