let n be Nat; :: thesis:
let F be FinSequence of (TOP-REAL n); :: thesis:
let fr be Function of (TOP-REAL n),REAL; :: thesis:
let Fv be FinSequence of (RealVectSpace (Seg n)); :: thesis:
let fv be Function of (RealVectSpace (Seg n)),REAL; :: thesis:
assume that
A1: fr = fv and
A2: F = Fv ; :: thesis:
A3: len (fv (#) Fv) = len Fv by RLVECT_2:def 7;
A4: len (fr (#) F) = len F by RLVECT_2:def 7;

reconsider T = TOP-REAL n as RealLinearSpace ;
let i be Nat; :: thesis:
reconsider Fi = F /. i as FinSequence of REAL by EUCLID:24;
A5: the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)

thus the carrier of (n -VectSp_over F_Real) = REAL n by MATRIX13:102
.= the carrier of (TOP-REAL n) by EUCLID:22 ; :: thesis:

end;

the carrier of (n -VectSp_over F_Real) = n -tuples_on the carrier of F_Real by MATRIX13:102;
then reconsider Fvi = Fv /. i as Element of n -tuples_on the carrier of F_Real by Lm1, A5;
reconsider Fii = F /. i as Element of T ;
assume A6: ( 1 <= i & i <= len F ) ; :: thesis:
then A7: i in dom (fv (#) Fv) by A2, A3, FINSEQ_3:25;
i in dom F by A6, FINSEQ_3:25;
then A8: F /. i = F . i by PARTFUN1:def 6;
A9: Fv /. i = Fv . i by A2, A6, FINSEQ_3:25, PARTFUN1:def 6;
i in dom (fr (#) F) by A4, A6, FINSEQ_3:25;
hence (fr (#) F) . i = (fr . Fii) * Fii by RLVECT_2:def 7
.= (fv . (Fv /. i)) * (Fv /. i) by A1, A2, A8, A9, EUCLID:65
.= (fv (#) Fv) . i by A7, RLVECT_2:def 7 ;
:: thesis:

end;

hence fr (#) F = fv (#) Fv by A2, A4, RLVECT_2:def 7; :: thesis: