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 GRAPH_5:sch 1();
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