deffunc H₁( 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₁(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