let r be Real; 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; for x being Element of REAL n st r <= 0 holds
product (Intervals (x,r)) is empty
let x be Element of REAL n; ( r <= 0 implies product (Intervals (x,r)) is empty )
assume A1:
r <= 0
; product (Intervals (x,r)) is empty
assume
not product (Intervals (x,r)) is empty
; 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; verum