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:
( 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 ) ) ) )

proof

assume A7: A = ].(inf A),(sup A).[ ; :: thesis:
A8: inf A <= sup A by XXREAL_2:40;
A9: for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t & B is 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 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 <> inf A & z2 <= sup A & z2 <> sup A ) by A7, A16, MEASURE5:def 2;
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;
1o < 1r by A7, A16, A18, MEASURE5:def 2;
then A20: x * 1o < x * 1r by A2, XREAL_1:70;
A21: 2o < 2r by A7, A16, A19, MEASURE5:def 2;
( 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, MEASURE5:def 2; :: 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 ;
q is R_eal by XXREAL_0:def 1;
then consider q1 being R_eal such that
A24: q1 = q ;
A25: ( d < q1 & q1 < g & q1 in REAL ) by A23, A24, MEASURE5:def 2;
A26: q = x * (q / x) by A2, XCMPLX_1:88;
set q2 = q / x;
q / x in A

proof

q / x is R_eal by XXREAL_0:def 1;
then consider q3 being R_eal such that
A27: q3 = q / x ;
( inf A < q3 & q3 < sup A & q3 in REAL )

proof

A28: q3 < sup A

proof

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

end;

inf A < q3

proof

A30: d < q1 by A23, A24, MEASURE5:def 2;
x * (q / x) = q by A2, XCMPLX_1:88;
hence inf A < q3 by A2, A10, A11, A24, A27, A30, XREAL_1:66; :: thesis:

end;

hence ( inf A < q3 & q3 < sup A & q3 in REAL ) by A27, A28; :: thesis:

end;

hence q / x in A by A7, A27, MEASURE5:def 2; :: thesis:

end;

hence q in x ** A by A26, 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 open_interval ) by A3, A11, A12, A13, MEASURE5:def 5, MEASURE6:38, MEASURE6:44; :: thesis:

end;

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

end;

( x <> 0 & A is open_interval ) by A2, A7, A8, MEASURE5:def 5;
then x ** A is open_interval by 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 A3, A9, MEASURE6:48; :: thesis:

end;

hence ( 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 ) ) ) ) ; :: thesis: