let A be Interval; :: thesis: for x, y being Real st 0 <= x & y = diameter A holds
x * y = diameter (x ** A)
let x, y be Real; :: thesis: ( 0 <= x & y = diameter A implies x * y = diameter (x ** A) )
assume that
A1: 0 <= x and
A2: y = diameter A ; :: thesis: x * y = diameter (x ** A)

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

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

then A4: x ** A is empty ;
thus x * y = 0 by A2, A3, MEASURE5:10
.= diameter (x ** A) by A4, MEASURE5:10 ; :: thesis: verum

end;

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

then consider z being Real such that
A6: z in A ;
reconsider z = z as Real ;
A7: x * z in x ** A by A6, MEMBER_1:193;
reconsider AA = A as non empty Subset of REAL by A5;
reconsider u = x as R_eal by XXREAL_0:def 1;
A8: inf (x ** AA) = u * (inf AA) by A1, Th19;
reconsider z = x as R_eal by XXREAL_0:def 1;
thus x * y = z * (diameter A) by A2, EXTREAL1:1
.= z * ((sup A) - (inf A)) by A5, MEASURE5:def 6
.= (z * (sup A)) - (z * (inf A)) by XXREAL_3:100
.= (sup (x ** A)) - (inf (x ** A)) by A1, A8, Th18
.= diameter (x ** A) by A7, MEASURE5:def 6 ; :: thesis: verum

end;

end;