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 ;
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