let n be Nat; 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); 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; 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)); 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; ( fr = fv & F = Fv implies fr (#) F = fv (#) Fv )
assume that
A1:
fr = fv
and
A2:
F = Fv
; 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 for i being Nat st 1 <= i & i <= len F holds
(fr (#) F) . i = (fv (#) Fv) . ireconsider T =
TOP-REAL n as
RealLinearSpace ;
let i be
Nat;
( 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)
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 )
;
(fr (#) F) . i = (fv (#) Fv) . ithen 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
;
verum end;
hence
fr (#) F = fv (#) Fv
by A2, A4, RLVECT_2:def 7; verum