let A be non empty Interval; :: thesis: for x being Real st 0 < x holds
for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).[ holds
( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
let x be Real; :: thesis: ( 0 < x implies for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).[ holds
( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
assume A1: 0 < x ; :: thesis: for B being non empty Interval st B = x ** A & A = [.(inf A),(sup A).[ holds
( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
let B be non empty Interval; :: thesis: ( B = x ** A & A = [.(inf A),(sup A).[ implies ( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
assume A2: B = x ** A ; :: thesis: ( not A = [.(inf A),(sup A).[ or ( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) )
A3: inf A <= sup A by XXREAL_2:40;
assume A4: A = [.(inf A),(sup A).[ ; :: thesis: ( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) )
then inf A <> sup A ;
then inf A < sup A by A3, XXREAL_0:1;
then inf A in A by A4, XXREAL_1:3;
then reconsider a = inf A as Real ;
A5: for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t & B is right_open_interval )

proof

let s, t be Real; :: thesis: ( s = inf A & t = sup A implies ( inf B = x * s & sup B = x * t & B is right_open_interval ) )
assume that
A6: s = inf A and
A7: t = sup A ; :: thesis: ( inf B = x * s & sup B = x * t & B is right_open_interval )
( inf B = x * s & sup B = x * t & B is right_open_interval )

proof

s <= t by A6, A7, XXREAL_2:40;
then A8: x * s <= x * t by A1, XREAL_1:64;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A9: d = x * s ;
x * t is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A10: g = x * t ;
A11: [.d,g.[ c= x ** A

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in [.d,g.[ or q in x ** A )
assume A12: q in [.d,g.[ ; :: thesis: q in x ** A
then reconsider q = q as Real by A9;
reconsider q2 = q / x as Element of REAL by XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A13: q1 < g by A12, XXREAL_1:3;
A14: q2 in A

proof

reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
( inf A <= q3 & q3 < sup A & q3 in REAL )

proof

A15: q3 < sup A

proof

consider p, o being Real such that
A16: ( p = q1 & o = g ) and
p <= o by A10, A13;
q1 < g by A12, XXREAL_1:3;
then p / x < o / x by A1, A16, XREAL_1:74;
hence q3 < sup A by A1, A7, A10, A16, XCMPLX_1:89; :: thesis: verum

end;

( d <= q1 & x * q2 = q ) by A1, A12, XCMPLX_1:87, XXREAL_1:3;
hence ( inf A <= q3 & q3 < sup A & q3 in REAL ) by A1, A6, A9, A15, XREAL_1:68; :: thesis: verum

end;

hence q2 in A by A4, XXREAL_1:3; :: thesis: verum

end;

q = x * (q / x) by A1, XCMPLX_1:87;
hence q in x ** A by A14, MEMBER_1:193; :: thesis: verum

end;

x ** A c= [.d,g.[

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in x ** A or q in [.d,g.[ )
assume A17: q in x ** A ; :: thesis: q in [.d,g.[
then reconsider q = q as Real ;
consider z2 being Real such that
A18: z2 in A and
A19: q = x * z2 by A17, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
z2 <= sup A by A4, A18, XXREAL_1:3;
then consider 2o, 2r being Real such that
A20: ( 2o = z2 & 2r = sup A ) and
2o <= 2r by A7;
( x * 2o is R_eal & x * 2r is R_eal ) by XXREAL_0:def 1;
then consider 2o1, 2r1 being R_eal such that
A21: ( 2o1 = x * 2o & 2r1 = x * 2r ) ;
2o < 2r by A4, A18, A20, XXREAL_1:3;
then A22: 2o1 < 2r1 by A1, A21, XREAL_1:68;
inf A <= z2 by A4, A18, XXREAL_1:3;
then consider 1o, 1ra being Real such that
A23: ( 1o = inf A & 1ra = z2 ) and
A24: 1o <= 1ra by A6;
x * 1o <= x * 1ra by A1, A24, XREAL_1:64;
hence q in [.d,g.[ by A6, A7, A9, A10, A19, A23, A20, A21, A22, XXREAL_1:3; :: thesis: verum

end;

then x ** A = [.d,g.[ by A11;
hence ( inf B = x * s & sup B = x * t & B is right_open_interval ) by A2, A9, A10, A8, MEASURE5:def 4, MEASURE6:11, MEASURE6:15; :: thesis: verum

end;

hence ( inf B = x * s & sup B = x * t & B is right_open_interval ) ; :: thesis: verum

end;

A = [.a,(sup A).[ by A4;
then A is right_open_interval by MEASURE5:def 4;
then x ** A is right_open_interval by A1, Th9;
hence ( B = [.(inf B),(sup B).[ & ( for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t ) ) ) by A2, A5, MEASURE6:18; :: thesis: verum