let n, i be Nat; :: thesis: for p being Element of (TOP-REAL n) ex q being Real ex g being FinSequence of REAL st
( g = p & q = g /. i )
let p be Element of (TOP-REAL n); :: thesis: ex q being Real ex g being FinSequence of REAL st
( g = p & q = g /. i )
p is Element of REAL n by EUCLID:22;
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 and
len s = n ;
s /. i = s /. i ;
hence ex q being Real ex g being FinSequence of REAL st
( g = p & q = g /. i ) by A1; :: thesis: verum