deffunc H_{1}( Real) -> Element of REAL = In ((f . ($1 + h)),REAL);

set X = (- h) ++ (dom f);

defpred S_{1}[ 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_{1}[x] ) ) & ( for x being Element of REAL st x in dom F holds

F . x = H_{1}(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)

F . x = f . (x + h) ; :: thesis: verum

set X = (- h) ++ (dom f);

defpred S

consider F being PartFunc of REAL,REAL such that

A1: ( ( for x being Element of REAL holds

( x in dom F iff S

F . x = H

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

hence
for x being Real st x in (- h) ++ (dom f) holds
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_{1}(x)
by A1;

hence F . x = f . (x + h) ; :: thesis: verum

end;assume x in (- h) ++ (dom f) ; :: thesis: F . x = f . (x + h)

then F . x = H

hence F . x = f . (x + h) ; :: thesis: verum

F . x = f . (x + h) ; :: thesis: verum