let t be Real; :: thesis: for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y)
let n be Element of NAT ; :: thesis: for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y)
let X, Y be Subset of (TOP-REAL n); :: thesis: ( t <> 0 implies t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y) )
assume A1: t <> 0 ; :: 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
A2: b = t * a and
A3: a in X (-) Y ;
consider x being Point of (TOP-REAL n) such that
A4: a = x and
A5: Y + x c= X by A3;
t (.) (Y + x) c= t (.) X by A5, Th61;
then (t (.) Y) + (t * x) c= t (.) X by Th62;
hence b in (t (.) X) (-) (t (.) Y) by A2, A4; :: 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 being Point of (TOP-REAL n) such that
A6: b = x and
A7: (t (.) Y) + x c= t (.) X ;
(1 / t) (.) ((t (.) Y) + x) c= (1 / t) (.) (t (.) X) by A7, Th61;
then (1 / t) (.) ((t (.) Y) + x) c= ((1 / t) * t) (.) X by Th60;
then ((1 / t) (.) (t (.) Y)) + ((1 / t) * x) c= ((1 / t) * t) (.) X by Th62;
then (((1 / t) * t) (.) Y) + ((1 / t) * x) c= ((1 / t) * t) (.) X by Th60;
then (1 (.) Y) + ((1 / t) * x) c= ((1 / t) * t) (.) X by A1, XCMPLX_1:87;
then (1 (.) Y) + ((1 / t) * x) c= 1 (.) X by A1, XCMPLX_1:87;
then Y + ((1 / t) * x) c= 1 (.) X by Th58;
then Y + ((1 / t) * x) c= X by Th58;
then (1 / t) * x in { z where z is Point of (TOP-REAL n) : Y + z c= X } ;
then t * ((1 / t) * x) in { (t * a1) where a1 is Point of (TOP-REAL n) : a1 in X (-) Y } ;
then ((1 / t) * t) * x in t (.) (X (-) Y) by RLVECT_1:def 7;
then 1 * x in t (.) (X (-) Y) by A1, XCMPLX_1:87;
hence b in t (.) (X (-) Y) by A6, RLVECT_1:def 8; :: thesis: verum