let p be FinSequence of 1 -tuples_on REAL; ( len p = 3 implies <*<*((p . 1) . 1)*>,<*((p . 2) . 1)*>,<*((p . 3) . 1)*>*> = p )
assume A1:
len p = 3
; <*<*((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; verum