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 :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> is FinSequence of 1 -tuples_on REAL
A8: ( <*(a * p1)*> in 1 -tuples_on REAL & <*(a * p2)*> in 1 -tuples_on REAL & <*(a * p3)*> in 1 -tuples_on REAL )

proof

a * p1 in REAL by XREAL_0:def 1;
hence <*(a * p1)*> in 1 -tuples_on REAL by FINSEQ_2:98; :: thesis: ( <*(a * p2)*> in 1 -tuples_on REAL & <*(a * p3)*> in 1 -tuples_on REAL )
a * p2 in REAL by XREAL_0:def 1;
hence <*(a * p2)*> in 1 -tuples_on REAL by FINSEQ_2:98; :: thesis: <*(a * p3)*> in 1 -tuples_on REAL
a * p3 in REAL by XREAL_0:def 1;
hence <*(a * p3)*> in 1 -tuples_on REAL by FINSEQ_2:98; :: thesis: verum

end;

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; :: thesis: verum

end;

hence ex b₁ 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 & b₁ = <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> ) ; :: thesis: verum