let p be FinSequence of 1 -tuples_on REAL; :: thesis: ( len p = 3 implies M2F p is Point of (TOP-REAL 3) )
assume A1: len p = 3 ; :: thesis: 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; :: thesis: verum