let r be Real; :: thesis: for n being non zero Nat
for x being Element of REAL n st r <= 0 holds
product (Intervals (x,r)) is empty
let n be non zero Nat; :: thesis: for x being Element of REAL n st r <= 0 holds
product (Intervals (x,r)) is empty
let x be Element of REAL n; :: thesis: ( r <= 0 implies product (Intervals (x,r)) is empty )
assume A1: r <= 0 ; :: thesis: product (Intervals (x,r)) is empty
assume not product (Intervals (x,r)) is empty ; :: thesis: contradiction
then consider t being object such that
A2: t in product (Intervals (x,r)) ;
consider g being Function such that
g = t and
dom g = dom (Intervals (x,r)) and
A3: for y being object st y in dom (Intervals (x,r)) holds
g . y in (Intervals (x,r)) . y by A2, CARD_3:def 5;
A4: dom x = Seg n by FINSEQ_2:124;
then A5: dom (Intervals (x,r)) = Seg n by EUCLID_9:def 3;
A6: ( n = 1 or n > 1 ) by NAT_1:53;
then 1 in dom (Intervals (x,r)) by A5;
then ( g . 1 in (Intervals (x,r)) . 1 & 1 in dom x ) by A3, A4, A6;
then not ].((x . 1) - r),((x . 1) + r).[ is empty by EUCLID_9:def 3;
hence contradiction by A1; :: thesis: verum