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

now :: thesis: for i being Nat st 1 <= i & i <= len F holds
(fr (#) F) . i = (fv (#) Fv) . i

reconsider T = TOP-REAL n as RealLinearSpace ;
let i be Nat; :: thesis: ( 1 <= i & i <= len F implies (fr (#) F) . i = (fv (#) Fv) . i )
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)

proof

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

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: (fr (#) F) . i = (fv (#) Fv) . i
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: verum

end;

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