let n be Element of NAT ; :: thesis: for B being Subset of (TOP-REAL n)
for t, s being real number st B is convex & 0 < t & 0 < s holds
(s + t) (.) B = (s (.) B) (+) (t (.) B)
let B be Subset of (TOP-REAL n); :: thesis: for t, s being real number st B is convex & 0 < t & 0 < s holds
(s + t) (.) B = (s (.) B) (+) (t (.) B)
let t, s be real number ; :: thesis: ( B is convex & 0 < t & 0 < s implies (s + t) (.) B = (s (.) B) (+) (t (.) B) )
assume A1: ( B is convex & 0 < t & 0 < s ) ; :: thesis: (s + t) (.) B = (s (.) B) (+) (t (.) B)
then A2: 0 + 0 < s + t ;
s < s + t by A1, XREAL_1:31;
then s / (s + t) < (s + t) / (s + t) by A1, XREAL_1:76;
then A4: s / (s + t) < 1 by A2, XCMPLX_1:60;
thus (s + t) (.) B c= (s (.) B) (+) (t (.) B) :: according to XBOOLE_0:def 10 :: thesis: (s (.) B) (+) (t (.) B) c= (s + t) (.) B

proof

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

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (s (.) B) (+) (t (.) B) or x in (s + t) (.) B )
assume x in (s (.) B) (+) (t (.) B) ; :: thesis: x in (s + t) (.) B
then consider s1, s2 being Point of (TOP-REAL n) such that
A8: ( x = s1 + s2 & s1 in s (.) B & s2 in t (.) B ) ;
consider b1 being Point of (TOP-REAL n) such that
A9: ( s1 = s * b1 & b1 in B ) by A8;
consider b2 being Point of (TOP-REAL n) such that
A10: ( s2 = t * b2 & b2 in B ) by A8;
((s / (s + t)) * b1) + ((1 - (s / (s + t))) * b2) in B by A1, A4, A9, A10, Def11;
then (s + t) * (((s / (s + t)) * b1) + ((1 - (s / (s + t))) * b2)) in { ((s + t) * zz) where zz is Point of (TOP-REAL n) : zz in B } ;
then ((s + t) * ((s / (s + t)) * b1)) + ((s + t) * ((1 - (s / (s + t))) * b2)) in (s + t) (.) B by EUCLID:36;
then (((s + t) * (s / (s + t))) * b1) + ((s + t) * ((1 - (s / (s + t))) * b2)) in (s + t) (.) B by EUCLID:34;
then (((s + t) * (s / (s + t))) * b1) + (((s + t) * (1 - (s / (s + t)))) * b2) in (s + t) (.) B by EUCLID:34;
then (s * b1) + (((s + t) * (1 - (s / (s + t)))) * b2) in (s + t) (.) B by A2, XCMPLX_1:88;
then (s * b1) + (((s + t) * (((s + t) / (s + t)) - (s / (s + t)))) * b2) in (s + t) (.) B by A2, XCMPLX_1:60;
then (s * b1) + (((s + t) * (((s + t) - s) / (s + t))) * b2) in (s + t) (.) B by XCMPLX_1:121;
hence x in (s + t) (.) B by A2, A8, A9, A10, XCMPLX_1:88; :: thesis: verum