deffunc H1( Real) -> Element of REAL = In ((f . (\$1 + h)),REAL);
set X = (- h) ++ (dom f);
defpred S1[ 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 S1[x] ) ) & ( for x being Element of REAL st x in dom F holds
F . x = H1(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 ; :: 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 = H1(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