let t, s be Real; for n being Element of NAT
for B being Subset of (TOP-REAL n) st B is convex & 0 < t & 0 < s holds
(s + t) (.) B = (s (.) B) (+) (t (.) B)
let n be Element of NAT ; for B being Subset of (TOP-REAL n) st B is convex & 0 < t & 0 < s holds
(s + t) (.) B = (s (.) B) (+) (t (.) B)
let B be Subset of (TOP-REAL n); ( B is convex & 0 < t & 0 < s implies (s + t) (.) B = (s (.) B) (+) (t (.) B) )
assume that
A1:
B is convex
and
A2:
( 0 < t & 0 < s )
; (s + t) (.) B = (s (.) B) (+) (t (.) B)
thus
(s + t) (.) B c= (s (.) B) (+) (t (.) B)
XBOOLE_0:def 10 (s (.) B) (+) (t (.) B) c= (s + t) (.) B
let x be object ; TARSKI:def 3 ( not x in (s (.) B) (+) (t (.) B) or x in (s + t) (.) B )
assume
x in (s (.) B) (+) (t (.) B)
; x in (s + t) (.) B
then consider s1, s2 being Point of (TOP-REAL n) such that
A6:
x = s1 + s2
and
A7:
s1 in s (.) B
and
A8:
s2 in t (.) B
;
consider b2 being Point of (TOP-REAL n) such that
A9:
s2 = t * b2
and
A10:
b2 in B
by A8;
consider b1 being Point of (TOP-REAL n) such that
A11:
s1 = s * b1
and
A12:
b1 in B
by A7;
s / (s + t) < (s + t) / (s + t)
by A2, XREAL_1:29, XREAL_1:74;
then
s / (s + t) < 1
by A2, XCMPLX_1:60;
then
((s / (s + t)) * b1) + ((1 - (s / (s + t))) * b2) in B
by A1, A2, A12, A10;
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 RLVECT_1:def 5;
then
(((s + t) * (s / (s + t))) * b1) + ((s + t) * ((1 - (s / (s + t))) * b2)) in (s + t) (.) B
by RLVECT_1:def 7;
then
(((s + t) * (s / (s + t))) * b1) + (((s + t) * (1 - (s / (s + t)))) * b2) in (s + t) (.) B
by RLVECT_1:def 7;
then
(s * b1) + (((s + t) * (1 - (s / (s + t)))) * b2) in (s + t) (.) B
by A2, XCMPLX_1:87;
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:120;
hence
x in (s + t) (.) B
by A2, A6, A11, A9, XCMPLX_1:87; verum