defpred S1[ object , object ] means $2 = product <*[.(a . $1),(b . $1).]*>;
A1: for x being object st x in NAT holds
ex y being object st
( y in bool (REAL 1) & S1[x,y] )
proof
let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in bool (REAL 1) & S1[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in bool (REAL 1) & S1[x,y] )
set y = product <*[.(a . x),(b . x).]*>;
take product <*[.(a . x),(b . x).]*> ; :: thesis: ( product <*[.(a . x),(b . x).]*> in bool (REAL 1) & S1[x, product <*[.(a . x),(b . x).]*>] )
product <*[.(a . x),(b . x).]*> c= REAL 1
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in product <*[.(a . x),(b . x).]*> or t in REAL 1 )
assume t in product <*[.(a . x),(b . x).]*> ; :: thesis: t in REAL 1
then consider f being Function such that
A2: t = f and
A3: dom f = dom <*[.(a . x),(b . x).]*> and
A4: for i being object st i in dom <*[.(a . x),(b . x).]*> holds
f . i in <*[.(a . x),(b . x).]*> . i by CARD_3:def 5;
A5: dom <*[.(a . x),(b . x).]*> = Seg 1 by FINSEQ_1:def 8;
A6: dom f = Seg 1 by A3, FINSEQ_1:def 8;
rng f c= REAL
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng f or u in REAL )
assume u in rng f ; :: thesis: u in REAL
then consider t being object such that
A7: t in dom f and
A8: u = f . t by FUNCT_1:def 3;
t in {1} by FINSEQ_1:2, A7, A3, FINSEQ_1:def 8;
then A9: ( t = 1 & 1 in Seg 1 ) by FINSEQ_1:2, TARSKI:def 1;
( u = f . 1 & 1 in dom <*[.(a . x),(b . x).]*> ) by A7, A3, FINSEQ_1:2, TARSKI:def 1, A8, A5;
then f . 1 in <*[.(a . x),(b . x).]*> . 1 by A4;
then u in [.(a . x),(b . x).] by A9, A8, FINSEQ_1:def 8;
hence u in REAL ; :: thesis: verum
end;
then t in Funcs ((Seg 1),REAL) by A2, FUNCT_2:def 2, A6;
then t in 1 -tuples_on REAL by FINSEQ_2:93;
hence t in REAL 1 by EUCLID:def 1; :: thesis: verum
end;
hence product <*[.(a . x),(b . x).]*> in bool (REAL 1) ; :: thesis: S1[x, product <*[.(a . x),(b . x).]*>]
thus S1[x, product <*[.(a . x),(b . x).]*>] ; :: thesis: verum
end;
ex f being Function of NAT,(bool (REAL 1)) st
for x being object st x in NAT holds
S1[x,f . x] from FUNCT_2:sch 1(A1);
 then consider f being Function of NAT,(bool (REAL 1)) such that
A10: for x being object st x in NAT holds
S1[x,f . x] ;
now :: thesis: ex f, f being Function of NAT,(bool (REAL 1)) st
for x being Nat holds S1[x,f . x]
take f = f; :: thesis: ex f being Function of NAT,(bool (REAL 1)) st
for x being Nat holds S1[x,f . x]
for x being Nat holds S1[x,f . x] by ORDINAL1:def 12, A10;
hence ex f being Function of NAT,(bool (REAL 1)) st
for x being Nat holds S1[x,f . x] ; :: thesis: verum
end;
hence ex b1 being SetSequence of (REAL 1) st
for i being Nat holds b1 . i = product <*[.(a . i),(b . i).]*> ; :: thesis: verum