let n be Nat; :: thesis: for F being FinSequence of ()
for fr being Function of (),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 (); :: thesis: for fr being Function of (),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 (),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 () = the carrier of ()
proof
thus the carrier of () = REAL n by MATRIX13:102
.= the carrier of () by EUCLID:22 ; :: thesis: verum
end;
the carrier of () = 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 ;
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 ;
i in dom F by ;
then A8: F /. i = F . i by PARTFUN1:def 6;
A9: Fv /. i = Fv . i by ;
i in dom (fr (#) F) by ;
hence (fr (#) F) . i = (fr . Fii) * Fii by RLVECT_2:def 7
.= (fv . (Fv /. i)) * (Fv /. i) by
.= (fv (#) Fv) . i by ;
:: thesis: verum
end;
hence fr (#) F = fv (#) Fv by ; :: thesis: verum