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 (n -VectSp_over F_Real); :: thesis:
let fv be Function of (n -VectSp_over F_Real),F_Real; :: thesis:
assume that
A1: fr = fv and
A2: F = Fv ; :: thesis:
A3: len (fv (#) Fv) = len Fv by VECTSP_6:def 5;
A4: len (fr (#) F) = len F by RLVECT_2:def 7;

now :: thesis:

reconsider T = TOP-REAL n as RealLinearSpace ;
let i be Nat; :: thesis:
reconsider Fi = F /. i as FinSequence of REAL by EUCLID:24;
reconsider Fvi = Fv /. i as Element of n -tuples_on the carrier of F_Real by MATRIX13:102;
reconsider Fii = F /. i as Element of T ;
assume A5: ( 1 <= i & i <= len F ) ; :: thesis:
then A6: i in dom (fv (#) Fv) by A2, A3, FINSEQ_3:25;
i in dom F by A5, FINSEQ_3:25;
then A7: F /. i = F . i by PARTFUN1:def 6;
i in dom Fv by A2, A5, FINSEQ_3:25;
then A8: Fv /. i = Fv . i by PARTFUN1:def 6;
i in dom (fr (#) F) by A4, A5, FINSEQ_3:25;
hence (fr (#) F) . i = (fr . Fii) * Fii by RLVECT_2:def 7
.= (fr . Fi) * Fi by EUCLID:65
.= (fv . (Fv /. i)) * Fvi by A1, A2, A7, A8, MATRIXR1:17
.= (fv . (Fv /. i)) * (Fv /. i) by MATRIX13:102
.= (fv (#) Fv) . i by A6, VECTSP_6:def 5 ;
:: thesis:

end;

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