let A be Interval; :: thesis: for x being Real st 0 <= x holds
for y being Real st y = diameter A holds
x * y = diameter (x ** A)
let x be Real; :: thesis: ( 0 <= x implies for y being Real st y = diameter A holds
x * y = diameter (x ** A) )
assume Z1: 0 <= x ; :: thesis: for y being Real st y = diameter A holds
x * y = diameter (x ** A)
let y be Real; :: thesis: ( y = diameter A implies x * y = diameter (x ** A) )
assume Z2: y = diameter A ; :: thesis: x * y = diameter (x ** A)

per cases ( A is empty or not A is empty ) ;

suppose S: A is empty ; :: thesis: x * y = diameter (x ** A)

X: now

assume not x ** A is empty ; :: thesis: contradiction
then consider y being real number such that
W: y in x ** A by MEMBERED:9;
reconsider y = y as Real by XREAL_0:def 1;
ex z being Real st
( z in A & y = x * z ) by W, INTEGRA2:def 2;
hence contradiction by S; :: thesis: verum

end;

thus x * y = 0 by S, Z2, MEASURE5:60
.= diameter (x ** A) by X, MEASURE5:60 ; :: thesis: verum

end;

suppose S: not A is empty ; :: thesis: x * y = diameter (x ** A)

then reconsider AA = A as non empty Subset of REAL ;
consider z being real number such that
W: z in A by S, MEMBERED:9;
reconsider z = z as Real by XREAL_0:def 1;
XX: x * z in x ** A by W, INTEGRA2:def 2;
reconsider z = x as R_eal by XXREAL_0:def 1;
reconsider u = x as R_eal by XXREAL_0:def 1;
Y2: inf (x ** AA) = u * (inf AA) by Tx2, Z1;
thus x * y = z * (diameter A) by Z2, EXTREAL1:13
.= z * ((sup A) - (inf A)) by S, MEASURE5:def 10
.= (z * (sup A)) - (z * (inf A)) by XXREAL_3:112
.= (sup (x ** A)) - (inf (x ** A)) by Tx1, Z1, Y2
.= diameter (x ** A) by XX, MEASURE5:def 10 ; :: thesis: verum

end;

end;