let p be FinSequence of 1 -tuples_on REAL; ( len p = 3 implies M2F p is Point of (TOP-REAL 3) )
assume A1:
len p = 3
; M2F p is Point of (TOP-REAL 3)
A2:
dom p = Seg 3
by A1, FINSEQ_1:def 3;
then A3:
p . 1 in rng p
by FINSEQ_1:1, FUNCT_1:3;
A4:
rng p c= 1 -tuples_on REAL
by FINSEQ_1:def 4;
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 A3, A4;
then consider d being Element of REAL such that
A5:
p . 1 = <*d*>
;
A6:
(p . 1) . 1 = d
by A5, FINSEQ_1:def 8;
A7:
p . 2 in rng p
by A2, FINSEQ_1:1, FUNCT_1:3;
1 -tuples_on REAL = { <*d*> where d is Element of REAL : verum }
by FINSEQ_2:96;
then
p . 2 in { <*d*> where d is Element of REAL : verum }
by A7, A4;
then consider d being Element of REAL such that
A9:
p . 2 = <*d*>
;
A10:
(p . 2) . 1 = d
by A9, FINSEQ_1:def 8;
A11:
p . 3 in rng p
by A2, FINSEQ_1:1, FUNCT_1:3;
rng p c= 1 -tuples_on REAL
by FINSEQ_1:def 4;
then A12:
p . 3 in 1 -tuples_on REAL
by A11;
1 -tuples_on REAL = { <*d*> where d is Element of REAL : verum }
by FINSEQ_2:96;
then consider d being Element of REAL such that
A13:
p . 3 = <*d*>
by A12;
A14:
(p . 3) . 1 = d
by A13, FINSEQ_1:def 8;
M2F p = <*((p . 1) . 1),((p . 2) . 1),((p . 3) . 1)*>
by A1, DEF2;
then
M2F p in 3 -tuples_on REAL
by A6, A10, A14, FINSEQ_2:104;
then
M2F p in REAL 3
by EUCLID:def 1;
hence
M2F p is Point of (TOP-REAL 3)
by EUCLID:22; verum