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