let t be Real; :: thesis: for n being Element of NAT
for X being Subset of (TOP-REAL n)
for x being Point of (TOP-REAL n) holds t (.) (X + x) = (t (.) X) + (t * x)
let n be Element of NAT ; :: thesis: for X being Subset of (TOP-REAL n)
for x being Point of (TOP-REAL n) 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) holds t (.) (X + x) = (t (.) X) + (t * x)
let x be Point of (TOP-REAL n); :: 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 object ; :: 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 and
A2: a in X + x ;
consider x1 being Point of (TOP-REAL n) such that
A3: a = x1 + x and
A4: x1 in X by A2;
A5: t * x1 in t (.) X by A4;
b = (t * x1) + (t * x) by A1, A3, RLVECT_1:def 5;
hence b in (t (.) X) + (t * x) by A5; :: thesis: verum

end;

let b be object ; :: 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
A6: b = x1 + (t * x) and
A7: x1 in t (.) X ;
consider a being Point of (TOP-REAL n) such that
A8: x1 = t * a and
A9: a in X by A7;
A10: a + x in X + x by A9;
b = t * (a + x) by A6, A8, RLVECT_1:def 5;
hence b in t (.) (X + x) by A10; :: thesis: verum