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 (n -VectSp_over F_Real)
for fv being Function of (n -VectSp_over F_Real),F_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 (n -VectSp_over F_Real)
for fv being Function of (n -VectSp_over F_Real),F_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 (n -VectSp_over F_Real)
for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
let Fv be FinSequence of (n -VectSp_over F_Real); :: thesis: for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
let fv be Function of (n -VectSp_over F_Real),F_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 VECTSP_6:def 5;
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;
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: (fr (#) F) . i = (fv (#) Fv) . i
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: verum

end;

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