let p be FinSequence of 1 -tuples_on REAL; :: thesis: ( len p = 3 implies <*<*((p . 1) . 1)*>,<*((p . 2) . 1)*>,<*((p . 3) . 1)*>*> = p )
assume A1: len p = 3 ; :: thesis: <*<*((p . 1) . 1)*>,<*((p . 2) . 1)*>,<*((p . 3) . 1)*>*> = p
then dom p = Seg 3 by 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*> ;
A6: (p . 1) . 1 = d1 by A5, FINSEQ_1:def 8;
p . 2 in { <*d*> where d is Element of REAL : verum } by A2, A3, A4;
then consider d2 being Element of REAL such that
A7: p . 2 = <*d2*> ;
A8: (p . 2) . 1 = d2 by A7, FINSEQ_1:def 8;
p . 3 in { <*d*> where d is Element of REAL : verum } by A2, A3, A4;
then consider d3 being Element of REAL such that
A9: p . 3 = <*d3*> ;
A10: (p . 3) . 1 = d3 by A9, FINSEQ_1:def 8;
thus <*<*((p . 1) . 1)*>,<*((p . 2) . 1)*>,<*((p . 3) . 1)*>*> = p by A5, A6, A7, A8, A9, A10, A1, FINSEQ_1:45; :: thesis: verum