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

proof

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

end;

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