deffunc H_{1}( Element of V) -> Element of the carrier of W = In ((f . ($1 + h)), the carrier of W);

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

defpred S_{1}[ 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_{1}[x] ) ) & ( for x being Element of V 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 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)

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

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

defpred S

consider F being PartFunc of V,W such that

A1: ( ( for x being Element of V holds

( x in dom F iff S

F . x = H

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

hence
for x being Element of V st x in (- h) ++ (dom f) holds
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_{1}(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;assume A3: x in (- h) ++ (dom f) ; :: thesis: F . x = f . (x + h)

then A4: F . x = H

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

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