deffunc H₁( Real) -> Element of REAL = In ((f . ($1 + h)),REAL);
set X = (- h) ++ (dom f);
defpred S₁[ set ] means $1 in (- h) ++ (dom f);
consider F being PartFunc of REAL,REAL such that
A1: ( ( for x being Element of REAL holds
( x in dom F iff S₁[x] ) ) & ( for x being Element of REAL st x in dom F holds
F . x = H₁(x) ) ) from SEQ_1:sch 3();
take F ; :: thesis: ( dom F = (- h) ++ (dom f) & ( for x being Real st x in (- h) ++ (dom f) holds
F . x = f . (x + h) ) )
for y being object st y in (- h) ++ (dom f) holds
y in dom F by A1;
then A2: (- h) ++ (dom f) c= dom F by TARSKI:def 3;
for y being object st y in dom F holds
y in (- h) ++ (dom f) by A1;
then dom F c= (- h) ++ (dom f) by TARSKI:def 3;
hence dom F = (- h) ++ (dom f) by A2, XBOOLE_0:def 10; :: thesis: for x being Real st x in (- h) ++ (dom f) holds
F . x = f . (x + h)
for x being Real st x in (- h) ++ (dom f) holds
F . x = f . (x + h)

proof

let x be Real; :: thesis: ( x in (- h) ++ (dom f) implies F . x = f . (x + h) )
assume x in (- h) ++ (dom f) ; :: thesis: F . x = f . (x + h)
then F . x = H₁(x) by A1;
hence F . x = f . (x + h) ; :: thesis: verum

end;

hence for x being Real st x in (- h) ++ (dom f) holds
F . x = f . (x + h) ; :: thesis: verum