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 ;
( x in NAT implies ex y being object st
( y in bool (REAL 1) & S1[x,y] ) )
assume
x in NAT
;
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).]*>
;
( 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 ;
TARSKI:def 3 ( not t in product <*[.(a . x),(b . x).]*> or t in REAL 1 )
assume
t in product <*[.(a . x),(b . x).]*>
;
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 ;
TARSKI:def 3 ( not u in rng f or u in REAL )
assume
u in rng f
;
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
;
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;
verum
end;
hence
product <*[.(a . x),(b . x).]*> in bool (REAL 1)
;
S1[x, product <*[.(a . x),(b . x).]*>]
thus
S1[
x,
product <*[.(a . x),(b . x).]*>]
;
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]
;
hence
ex b1 being SetSequence of (REAL 1) st
for i being Nat holds b1 . i = product <*[.(a . i),(b . i).]*>
; verum