defpred S1[ object , object ] means ex S being Subset of REAL st
( S = $2 & S = [.(a . $1),(b . $1).] );
A1:
for i being Nat st i in Seg n holds
ex d being Element of bool REAL st S1[i,d]
;
consider f being FinSequence of bool REAL such that
A2:
len f = n
and
A3:
for i being Nat st i in Seg n holds
S1[i,f /. i]
from FINSEQ_4:sch 1(A1);
A4:
dom f = Seg n
by A2, FINSEQ_1:def 3;
set s = product f;
product f c= product ((Seg n) --> REAL)
then reconsider s = product f as Subset of (REAL n) by Th7;
for x being object holds
( x in s iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).] ) ) )
proof
let x be
object ;
( x in s iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).] ) ) )
thus
(
x in s iff ex
y being
Element of
REAL n st
(
x = y & ( for
i being
Nat st
i in Seg n holds
y . i in [.(a . i),(b . i).] ) ) )
verumproof
hereby ( ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).] ) ) implies x in s )
assume A8:
x in s
;
ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).] ) )then reconsider y =
x as
Element of
REAL n ;
take y =
y;
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).] ) )thus
x = y
;
for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).]thus
for
i being
Nat st
i in Seg n holds
y . i in [.(a . i),(b . i).]
verumproof
let i be
Nat;
( i in Seg n implies y . i in [.(a . i),(b . i).] )
assume A9:
i in Seg n
;
y . i in [.(a . i),(b . i).]
then A10:
i in dom f
by A2, FINSEQ_1:def 3;
then A11:
y . i in f . i
by A8, CARD_3:9;
consider S2 being
Subset of
REAL such that A12:
f /. i = S2
and A13:
S2 = [.(a . i),(b . i).]
by A9, A3;
thus
y . i in [.(a . i),(b . i).]
by A10, A11, A12, A13, PARTFUN1:def 6;
verum
end;
end;
given y being
Element of
REAL n such that A14:
x = y
and A15:
for
i being
Nat st
i in Seg n holds
y . i in [.(a . i),(b . i).]
;
x in s
hence
x in s
by A14, CARD_3:9;
verum
end;
end;
hence
ex b1 being Subset of (REAL n) st
for x being object holds
( x in b1 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).] ) ) )
; verum