let A be non empty Interval; :: thesis:
let x be Real; :: thesis:
assume A2: 0 < x ; :: thesis:
let B be non empty Interval; :: thesis:
assume A3: B = x ** A ; :: thesis:
assume A7: A = [.(inf A),(sup A).[ ; :: thesis:
A8: inf A <= sup A by XXREAL_2:40;
inf A <> sup A by A7;
then inf A < sup A by A8, XXREAL_0:1;
then inf A in A by A7, XXREAL_1:3;
then reconsider a = inf A as real number ;
X: A = [.a,(sup A).[ by A7;
A9: 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:
assume A10: ( s = inf A & t = sup A ) ; :: thesis:
( inf B = x * s & sup B = x * t & B is right_open_interval )

proof

x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A11: d = x * s ;
x * t is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A12: g = x * t ;
A13: x ** A = [.d,g.[

proof

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

proof

let q be set ; :: according to TARSKI:def 3 :: thesis:
assume A15: q in x ** A ; :: thesis:
then reconsider q = q as Real ;
consider z2 being Real such that
A16: ( z2 in A & q = x * z2 ) by A15, INTEGRA2:def 2;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
A17: ( inf A <= z2 & z2 <= sup A & z2 <> sup A ) by A7, A16, XXREAL_1:3;
then consider 1o, 1r being Real such that
A18: ( 1o = inf A & 1r = z2 & 1o <= 1r ) by A10;
consider 2o, 2r being Real such that
A19: ( 2o = z2 & 2r = sup A & 2o <= 2r ) by A10, A17;
A20: x * 1o <= x * 1r by A2, A18, XREAL_1:66;
A21: 2o < 2r by A7, A16, A19, XXREAL_1:3;
( x * 2o is R_eal & x * 2r is R_eal ) by XXREAL_0:def 1;
then consider 2o1, 2r1 being R_eal such that
A22: ( 2o1 = x * 2o & 2r1 = x * 2r ) ;
2o1 < 2r1 by A2, A21, A22, XREAL_1:70;
hence q in [.d,g.[ by A10, A11, A12, A16, A18, A19, A20, A22, XXREAL_1:3; :: thesis:

end;

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

proof

let q be set ; :: according to TARSKI:def 3 :: thesis:
assume A23: q in [.d,g.[ ; :: thesis:
then reconsider q = q as Real by A11, XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A24: ( d <= q1 & q1 < g & q1 in REAL ) by A23, XXREAL_1:3;
A25: q = x * (q / x) by A2, XCMPLX_1:88;
set q2 = q / x;
q / x in A

proof

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

proof

A26: q3 < sup A

proof

A27: q1 < g by A23, XXREAL_1:3;
consider p, o being Real such that
A28: ( p = q1 & o = g & p <= o ) by A12, A24;
p / x < o / x by A2, A27, A28, XREAL_1:76;
hence q3 < sup A by A2, A10, A12, A28, XCMPLX_1:90; :: thesis:

end;

d <= q1 by A23, XXREAL_1:3;
then consider t, o being Real such that
A29: ( t = d & o = q1 & t <= o ) by A11;
x * (q / x) = q by A2, XCMPLX_1:88;
hence ( inf A <= q3 & q3 < sup A & q3 in REAL ) by A2, A10, A11, A26, A29, XREAL_1:70; :: thesis:

end;

hence q / x in A by A7, XXREAL_1:3; :: thesis:

end;

hence q in x ** A by A25, INTEGRA2:def 2; :: thesis:

end;

hence x ** A = [.d,g.[ by A14, XBOOLE_0:def 10; :: thesis:

end;

s <= t by A10, XXREAL_2:40;
then x * s <= x * t by A2, XREAL_1:66;
hence ( inf B = x * s & sup B = x * t & B is right_open_interval ) by A3, A11, A12, A13, MEASURE5:def 7, MEASURE6:41, MEASURE6:47; :: thesis:

end;

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

end;

A is right_open_interval by A8, X, MEASURE5:def 7;
then x ** A is right_open_interval by A2, Th11;
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 A3, A9, MEASURE6:50; :: thesis: