theorem Th19: :: REAL_NS2:19

for n being Nat
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