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 ) ) ) )
( 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: ( 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;
then Y: ( inf A in A & sup A in A ) by A7, XXREAL_1:1;
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;
A17: ( inf A <= z2 & z2 <= sup A ) by A7, A16, XXREAL_1:1;
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;
( 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 ) ;
2o1 <= 2r1 by A2, A19, A21, XREAL_1:66;
hence q in [.d,g.] by A10, A11, A12, A16, A18, A19, A20, A21, XXREAL_1:1; :: 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 A11, 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

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

proof

A25: q3 <= sup A

proof

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

end;

inf A <= q3

proof

d <= q1 by A22, XXREAL_1:1;
then consider t, o being Real such that
A27: ( t = d & o = q1 & t <= o ) by A11;
x * (q / x) = q by A2, XCMPLX_1:88;
hence inf A <= q3 by A2, A10, A11, A24, A27, XREAL_1:70; :: thesis: verum

end;

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

end;

hence q / x in A by A7, A24, XXREAL_1:1; :: 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:40, MEASURE6:46; :: thesis: verum

end;

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

end;

A is closed_interval by A7, A8, Y, MEASURE5:def 6;
then x ** A is closed_interval by Th10, 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 A3, A9, MEASURE6:49; :: thesis: verum

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: verum