let n, i be Element of NAT ; :: thesis: for p being Element of (TOP-REAL n) ex q being Real st
for g being FinSequence of REAL st g = p holds
q = g /. i
let p be Element of (TOP-REAL n); :: thesis: ex q being Real st
for g being FinSequence of REAL st g = p holds
q = g /. i
p is Element of REAL n by EUCLID:25;
then p in { s where s is Element of REAL * : len s = n } ;
then consider s being Element of REAL * such that
A1: ( p = s & len s = n ) ;
for g being FinSequence of REAL st g = p holds
s /. i = g /. i by A1;
hence ex q being Real st
for g being FinSequence of REAL st g = p holds
q = g /. i ; :: thesis: verum