deffunc H1( Element of V) -> Element of the carrier of W = In ((f . (\$1 + h)), the carrier of W);
set X = (- h) ++ (dom f);
defpred S1[ set ] means \$1 in (- h) ++ (dom f);
consider F being PartFunc of V,W such that
A1: ( ( for x being Element of V holds
( x in dom F iff S1[x] ) ) & ( for x being Element of V 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 Element of V 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 Element of V st x in (- h) ++ (dom f) holds
F . x = f . (x + h)

for x being Element of V st x in (- h) ++ (dom f) holds
F . x = f . (x + h)
proof
let x be Element of V; :: thesis: ( x in (- h) ++ (dom f) implies F . x = f . (x + h) )
assume A3: x in (- h) ++ (dom f) ; :: thesis: F . x = f . (x + h)
then A4: F . x = H1(x) by A1;
consider u being Element of V such that
A5: ( x = (- h) + u & u in dom f ) by A3;
x + h = u + ((- h) + h) by
.= u + (0. V) by VECTSP_1:16
.= u by RLVECT_1:def 4 ;
hence F . x = f . (x + h) by ; :: thesis: verum
end;
hence for x being Element of V st x in (- h) ++ (dom f) holds
F . x = f . (x + h) ; :: thesis: verum