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)
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in product f or t in product ((Seg n) --> REAL) )
assume A5: t in product f ; :: thesis: t in product ((Seg n) --> REAL)
then reconsider t1 = t as Function ;
A6: ( dom t1 = dom f & ( for y being object st y in dom f holds
t1 . y in f . y ) ) by A5, CARD_3:9;
now :: thesis: ( dom t1 = dom ((Seg n) --> REAL) & ( for y being object st y in dom ((Seg n) --> REAL) holds
t1 . y in ((Seg n) --> REAL) . y ) )
dom ((Seg n) --> REAL) = Seg n by FUNCOP_1:13;
hence dom t1 = dom ((Seg n) --> REAL) by A6, A2, FINSEQ_1:def 3; :: thesis: for y being object st y in dom ((Seg n) --> REAL) holds
t1 . y in ((Seg n) --> REAL) . y
thus for y being object st y in dom ((Seg n) --> REAL) holds
t1 . y in ((Seg n) --> REAL) . y :: thesis: verum
proof
let y be object ; :: thesis: ( y in dom ((Seg n) --> REAL) implies t1 . y in ((Seg n) --> REAL) . y )
assume A7: y in dom ((Seg n) --> REAL) ; :: thesis: t1 . y in ((Seg n) --> REAL) . y
then y in Seg n ;
then y in dom f by A2, FINSEQ_1:def 3;
then ( t1 . y in f . y & f . y in bool REAL ) by A5, CARD_3:9, FINSEQ_2:11;
then t1 . y in REAL ;
hence t1 . y in ((Seg n) --> REAL) . y by A7, FUNCOP_1:7; :: thesis: verum
end;
end;
hence t in product ((Seg n) --> REAL) by CARD_3:9; :: thesis: verum
end;
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 ; :: thesis: ( 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).] ) ) ) :: thesis: verum
proof
hereby :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).] ) )
thus x = y ; :: thesis: 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).] :: thesis: verum
proof
let i be Nat; :: thesis: ( i in Seg n implies y . i in [.(a . i),(b . i).] )
assume A9: i in Seg n ; :: thesis: 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; :: thesis: 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).] ; :: thesis: x in s
now :: thesis: ( dom y = dom f & ( for z being object st z in dom f holds
y . z in f . z ) )
thus dom y = dom f by A4, FINSEQ_1:89; :: thesis: for z being object st z in dom f holds
y . z in f . z
thus for z being object st z in dom f holds
y . z in f . z :: thesis: verum
proof
let z be object ; :: thesis: ( z in dom f implies y . z in f . z )
assume A16: z in dom f ; :: thesis: y . z in f . z
then A17: z in Seg n by A2, FINSEQ_1:def 3;
then consider S2 being Subset of REAL such that
A18: f /. z = S2 and
A19: S2 = [.(a . z),(b . z).] by A3;
f /. z = f . z by A16, PARTFUN1:def 6;
hence y . z in f . z by A18, A19, A15, A17; :: thesis: verum
end;
end;
hence x in s by A14, CARD_3:9; :: thesis: 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).] ) ) ) ; :: thesis: verum