deffunc H₁( Element of V) -> Element of the carrier of W = In ((f . ($1 + h)), the carrier of W);
set X = (- h) ++ (dom f);
defpred S₁[ 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 S₁[x] ) ) & ( for x being Element of V 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 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 A2, XBOOLE_0:def 10; :: 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 = H₁(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 RLVECT_1:def 3, A5
.= u + (0. V) by VECTSP_1:16
.= u by RLVECT_1:def 4 ;
hence F . x = f . (x + h) by A4, SUBSET_1:def 8, PARTFUN1:4, A5; :: thesis: verum

end;

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