let x, y be Element of REAL n; :: according to EUCLID_7:def 8 :: thesis: for a, b being Element of REAL st x in [#] (REAL n) & y in [#] (REAL n) holds
(a * x) + (b * y) in [#] (REAL n)
let a, b be Element of REAL ; :: thesis: ( x in [#] (REAL n) & y in [#] (REAL n) implies (a * x) + (b * y) in [#] (REAL n) )
assume that
x in [#] (REAL n) and
y in [#] (REAL n) ; :: thesis: (a * x) + (b * y) in [#] (REAL n)
(a * x) + (b * y) in REAL n ;
hence (a * x) + (b * y) in [#] (REAL n) by SUBSET_1:def 3; :: thesis: verum