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 ) ) ) )
( 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 A3: 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 ) ) )
A4: 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 that
A5: s = inf A and
A6: t = sup A ; :: thesis: ( inf B = x * s & sup B = x * t )
( inf B = x * s & sup B = x * t )

proof

s <= t by A5, A6, XXREAL_2:40;
then A7: 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
A8: d = x * s ;
x * t is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A9: g = x * t ;
A10: [.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 A11: q in [.d,g.] ; :: thesis: q in x ** A
then reconsider q = q as Real by A8, A9;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A12: q / x in A

proof

reconsider q3 = q / x as R_eal by XXREAL_0:def 1;
A14: q3 <= sup A

proof

q1 <= g by A11, XXREAL_1:1;
then consider p, o being Real such that
A15: ( p = q1 & o = g ) and
A16: p <= o by A9;
p / x <= o / x by A1, A16, XREAL_1:72;
hence q3 <= sup A by A1, A6, A9, A15, XCMPLX_1:89; :: thesis: verum

end;

inf A <= q3

proof

( d <= q1 & x * (q / x) = q ) by A1, A11, XCMPLX_1:87, XXREAL_1:1;
hence inf A <= q3 by A1, A5, A8, XREAL_1:68; :: thesis: verum

end;

hence q / x in A by A3, A14, XXREAL_1:1; :: thesis: verum

end;

q = x * (q / x) by A1, XCMPLX_1:87;
hence q in x ** A by A12, 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;
inf A <= z2 by A3, A18, XXREAL_1:1;
then consider 1o, 1ra being Real such that
A20: ( 1o = inf A & 1ra = z2 ) and
A21: 1o <= 1ra by A5;
A22: x * 1o <= x * 1ra by A1, A21, XREAL_1:64;
z2 <= sup A by A3, A18, XXREAL_1:1;
then consider 2o, 2r being Real such that
A23: ( 2o = z2 & 2r = sup A ) and
A24: 2o <= 2r by A6;
( x * 2o is R_eal & x * 2r is R_eal ) by XXREAL_0:def 1;
then consider 2o1, 2r1 being R_eal such that
A25: ( 2o1 = x * 2o & 2r1 = x * 2r ) ;
2o1 <= 2r1 by A1, A24, A25, XREAL_1:64;
hence q in [.d,g.] by A5, A6, A8, A9, A19, A20, A23, A22, A25, XXREAL_1:1; :: thesis: verum

end;

then x ** A = [.d,g.] by A10;
hence ( inf B = x * s & sup B = x * t ) by A2, A8, A9, A7, MEASURE6:10, MEASURE6:14; :: thesis: verum

end;

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

end;

inf A <= sup A by XXREAL_2:40;
then ( inf A in A & sup A in A ) by A3, XXREAL_1:1;
then A is closed_interval by A3, MEASURE5:def 3;
then x ** A is closed_interval by A1, Th8;
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, A4, MEASURE6:17; :: 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