let n be Nat; :: thesis: for Fr being FinSequence of (TOP-REAL n)
for fr being Function of (TOP-REAL n),REAL
for Fv being FinSequence of (REAL-NS n)
for fv being Function of (REAL-NS n),REAL st fr = fv & Fr = Fv holds
fr (#) Fr = fv (#) Fv
let Fr be FinSequence of (TOP-REAL n); :: thesis: for fr being Function of (TOP-REAL n),REAL
for Fv being FinSequence of (REAL-NS n)
for fv being Function of (REAL-NS n),REAL st fr = fv & Fr = Fv holds
fr (#) Fr = fv (#) Fv
let fr be Function of (TOP-REAL n),REAL; :: thesis: for Fv being FinSequence of (REAL-NS n)
for fv being Function of (REAL-NS n),REAL st fr = fv & Fr = Fv holds
fr (#) Fr = fv (#) Fv
let Fv be FinSequence of (REAL-NS n); :: thesis: for fv being Function of (REAL-NS n),REAL st fr = fv & Fr = Fv holds
fr (#) Fr = fv (#) Fv
let fv be Function of (REAL-NS n),REAL; :: thesis: ( fr = fv & Fr = Fv implies fr (#) Fr = fv (#) Fv )
assume A1: ( fr = fv & Fr = Fv ) ; :: thesis: fr (#) Fr = fv (#) Fv
then A2: len (fv (#) Fv) = len Fr by RLVECT_2:def 7;
A3: fv (#) Fv is FinSequence of (TOP-REAL n) by Th4;
for i being Nat st i in dom (fv (#) Fv) holds
(fv (#) Fv) . i = (fr . (Fr /. i)) * (Fr /. i)

proof

let i be Nat; :: thesis: ( i in dom (fv (#) Fv) implies (fv (#) Fv) . i = (fr . (Fr /. i)) * (Fr /. i) )
assume A4: i in dom (fv (#) Fv) ; :: thesis: (fv (#) Fv) . i = (fr . (Fr /. i)) * (Fr /. i)
A5: Fv /. i = Fr /. i by A1, Th4;
thus (fv (#) Fv) . i = (fv . (Fv /. i)) * (Fv /. i) by A4, RLVECT_2:def 7
.= (fr . (Fr /. i)) * (Fr /. i) by A1, A5, Th8 ; :: thesis: verum

end;

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