let n be Nat; :: thesis: for X being Subspace of REAL-L 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 REAL-L 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 A1: ( x in the carrier of X & y in the carrier of X ) ; :: thesis: (a * x) + y in the carrier of X
reconsider x1 = x, y1 = y as Element of (REAL-L n) ;
a * x in the carrier of X by Th42, A1;
hence (a * x) + y in the carrier of X by Th43, A1; :: thesis: verum