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 A2: 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 A3: 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 ) ) ) )
assume A7: 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 ) ) )
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 sup A in A by A7, XXREAL_1:2;
then reconsider b = sup A as real number ;
X: A = ].(inf A),b.] by A7;
A9: for s, t being Real st s = inf A & t = sup A holds
( inf B = x * s & sup B = x * t )

proof

let s, t be Real; :: thesis: ( s = inf A & t = sup A implies ( inf B = x * s & sup B = x * t ) )
assume A10: ( s = inf A & t = sup A ) ; :: thesis: ( inf B = x * s & sup B = x * t )
( inf B = x * s & sup B = x * t )

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: ( not q in x ** A or q in ].d,g.] )
assume A15: q in x ** A ; :: thesis: q in ].d,g.]
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;
reconsider q = q as R_eal by XXREAL_0:def 1;
A17: ( inf A <= z2 & z2 <> inf A & z2 <= sup A ) by A7, A16, XXREAL_1: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;
A20: 1o < 1r by A7, A16, A18, XXREAL_1:2;
A21: x * 2o <= x * 2r by A2, A19, XREAL_1:66;
d < q by A2, A10, A11, A16, A18, A20, XREAL_1:70;
hence q in ].d,g.] by A10, A12, A16, A19, A21, XXREAL_1:2; :: thesis: verum

end;

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

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in ].d,g.] or q in x ** A )
assume A22: q in ].d,g.] ; :: thesis: q in x ** A
then reconsider q = q as Real by A12, XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
set q2 = q / x;
A23: 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

A24: q3 <= sup A

proof

q1 <= g by A22, XXREAL_1:2;
then consider p, o being Real such that
A25: ( p = q1 & o = g & p <= o ) by A12;
p / x <= o / x by A2, A25, XREAL_1:74;
hence q3 <= sup A by A2, A10, A12, A25, XCMPLX_1:90; :: thesis: verum

end;

inf A < q3

proof

A26: d < q1 by A22, XXREAL_1:2;
x * (q / x) = q by A2, XCMPLX_1:88;
hence inf A < q3 by A2, A10, A11, A26, XREAL_1:66; :: thesis: verum

end;

hence ( inf A < q3 & q3 <= sup A & q3 in REAL ) by A24; :: thesis: verum

end;

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

end;

q = x * (q / x) by A2, XCMPLX_1:88;
hence q in x ** A by A23, INTEGRA2:def 2; :: thesis: verum

end;

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

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 ) by A3, A11, A12, A13, MEASURE6:39, MEASURE6:45; :: thesis: verum

end;

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

end;

A is left_open_interval by A8, X, MEASURE5:def 8;
then B is left_open_interval by A3, Th13, A2;
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 A9, MEASURE6:51; :: thesis: verum