let n be Element of NAT ; :: thesis: for X being Subset of (TOP-REAL n)
for x being Point of (TOP-REAL n)
for t being real number holds t (.) (X + x) = (t (.) X) + (t * x)
let X be Subset of (TOP-REAL n); :: thesis: for x being Point of (TOP-REAL n)
for t being real number holds t (.) (X + x) = (t (.) X) + (t * x)
let x be Point of (TOP-REAL n); :: thesis: for t being real number holds t (.) (X + x) = (t (.) X) + (t * x)
let t be real number ; :: thesis: t (.) (X + x) = (t (.) X) + (t * x)
thus t (.) (X + x) c= (t (.) X) + (t * x) :: according to XBOOLE_0:def 10 :: thesis: (t (.) X) + (t * x) c= t (.) (X + x)

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in t (.) (X + x) or b in (t (.) X) + (t * x) )
assume b in t (.) (X + x) ; :: thesis: b in (t (.) X) + (t * x)
then consider a being Point of (TOP-REAL n) such that
A1: ( b = t * a & a in X + x ) ;
consider x1 being Point of (TOP-REAL n) such that
A2: ( a = x1 + x & x1 in X ) by A1;
A3: b = (t * x1) + (t * x) by A1, A2, EUCLID:36;
t * x1 in t (.) X by A2;
hence b in (t (.) X) + (t * x) by A3; :: thesis: verum

end;

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in (t (.) X) + (t * x) or b in t (.) (X + x) )
assume b in (t (.) X) + (t * x) ; :: thesis: b in t (.) (X + x)
then consider x1 being Point of (TOP-REAL n) such that
A4: ( b = x1 + (t * x) & x1 in t (.) X ) ;
consider a being Point of (TOP-REAL n) such that
A5: ( x1 = t * a & a in X ) by A4;
A6: b = t * (a + x) by A4, A5, EUCLID:36;
a + x in X + x by A5;
hence b in t (.) (X + x) by A6; :: thesis: verum