deffunc H_{1}( Element of REAL ) -> FinSequence of REAL = Replace (x,i,$1);

consider f being Function such that

A1: ( dom f = REAL & ( for r being Element of REAL st r in REAL holds

f . r = H_{1}(r) ) )
from CLASSES1:sch 2();

take f ; :: thesis: ( dom f = REAL & ( for r being Element of REAL holds f . r = Replace (x,i,r) ) )

thus ( dom f = REAL & ( for r being Element of REAL holds f . r = Replace (x,i,r) ) ) by A1; :: thesis: verum

consider f being Function such that

A1: ( dom f = REAL & ( for r being Element of REAL st r in REAL holds

f . r = H

take f ; :: thesis: ( dom f = REAL & ( for r being Element of REAL holds f . r = Replace (x,i,r) ) )

thus ( dom f = REAL & ( for r being Element of REAL holds f . r = Replace (x,i,r) ) ) by A1; :: thesis: verum