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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (t * s) (.) X or x in t (.) (s (.) X) )
assume x in (t * s) (.) X ; :: thesis: x in t (.) (s (.) X)
then consider z being Point of (TOP-REAL n) such that
A1: ( x = (t * s) * z & z in X ) ;
( x = t * (s * z) & s * z in s (.) X ) by A1, RLVECT_1:def 7;
hence x in t (.) (s (.) X) ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in t (.) (s (.) X) or x in (t * s) (.) X )
assume x in t (.) (s (.) X) ; :: thesis: x in (t * s) (.) X
then consider z being Point of (TOP-REAL n) such that
A2: x = t * z and
A3: z in s (.) X ;
consider z1 being Point of (TOP-REAL n) such that
A4: z = s * z1 and
A5: z1 in X by A3;
x = (t * s) * z1 by A2, A4, RLVECT_1:def 7;
hence x in (t * s) (.) X by A5; :: thesis: verum