dom p = Seg 3
by A1, FINSEQ_1:def 3;
then A2:
( p . 1 in rng p & p . 2 in rng p & p . 3 in rng p )
by FINSEQ_1:1, FUNCT_1:3;
A3:
rng p c= 1 -tuples_on REAL
by FINSEQ_1:def 4;
A4:
1 -tuples_on REAL = { <*d*> where d is Element of REAL : verum }
by FINSEQ_2:96;
then
p . 1 in { <*d*> where d is Element of REAL : verum }
by A2, A3;
then consider d1 being Element of REAL such that
A5:
p . 1 = <*d1*>
;
reconsider p1 = d1 as Real ;
p . 2 in { <*d*> where d is Element of REAL : verum }
by A2, A3, A4;
then consider d2 being Element of REAL such that
A6:
p . 2 = <*d2*>
;
reconsider p2 = d2 as Real ;
p . 3 in { <*d*> where d is Element of REAL : verum }
by A4, A2, A3;
then consider d3 being Element of REAL such that
A7:
p . 3 = <*d3*>
;
reconsider p3 = d3 as Real ;
now ex p1, p2, p3 being Real st
( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> is FinSequence of 1 -tuples_on REAL )take p1 =
p1;
ex p2, p3 being Real st
( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> is FinSequence of 1 -tuples_on REAL )take p2 =
p2;
ex p3 being Real st
( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> is FinSequence of 1 -tuples_on REAL )take p3 =
p3;
( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> is FinSequence of 1 -tuples_on REAL )thus
(
p1 = (p . 1) . 1 &
p2 = (p . 2) . 1 &
p3 = (p . 3) . 1 )
by A5, A6, A7, FINSEQ_1:def 8;
<*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> is FinSequence of 1 -tuples_on REALA8:
(
<*(a * p1)*> in 1
-tuples_on REAL &
<*(a * p2)*> in 1
-tuples_on REAL &
<*(a * p3)*> in 1
-tuples_on REAL )
A9:
rng <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> = {<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>}
by FINSEQ_2:128;
{<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>} c= 1
-tuples_on REAL
by A8, ENUMSET1:def 1;
hence
<*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> is
FinSequence of 1
-tuples_on REAL
by A9, FINSEQ_1:def 4;
verum end;
hence
ex b1 being FinSequence of 1 -tuples_on REAL ex p1, p2, p3 being Real st
( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & b1 = <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> )
; verum