for IT being Function of REAL,REAL holds

( IT = Shift (f,h) iff for x being Real holds IT . x = f . (x + h) )_{1} being Function of REAL,REAL holds

( b_{1} = Shift (f,h) iff for x being Real holds b_{1} . x = f . (x + h) )
; :: thesis: verum

( IT = Shift (f,h) iff for x being Real holds IT . x = f . (x + h) )

proof

hence
for b
let IT be Function of REAL,REAL; :: thesis: ( IT = Shift (f,h) iff for x being Real holds IT . x = f . (x + h) )

then dom (Shift (f,h)) = REAL by MEASURE6:24;

then A2: dom IT = dom (Shift (f,h)) by FUNCT_2:def 1;

assume A3: for x being Real holds IT . x = f . (x + h) ; :: thesis: IT = Shift (f,h)

for x being Element of REAL st x in dom IT holds

IT . x = (Shift (f,h)) . x

end;hereby :: thesis: ( ( for x being Real holds IT . x = f . (x + h) ) implies IT = Shift (f,h) )

( dom (Shift (f,h)) = (- h) ++ (dom f) & dom f = REAL )
by Def1, FUNCT_2:def 1;assume A1:
IT = Shift (f,h)
; :: thesis: for x being Real holds IT . x = f . (x + h)

let x be Real; :: thesis: IT . x = f . (x + h)

dom (Shift (f,h)) = REAL by A1, FUNCT_2:def 1;

then x in dom (Shift (f,h)) by XREAL_0:def 1;

then x in (- h) ++ (dom f) by Def1;

hence IT . x = f . (x + h) by A1, Def1; :: thesis: verum

end;let x be Real; :: thesis: IT . x = f . (x + h)

dom (Shift (f,h)) = REAL by A1, FUNCT_2:def 1;

then x in dom (Shift (f,h)) by XREAL_0:def 1;

then x in (- h) ++ (dom f) by Def1;

hence IT . x = f . (x + h) by A1, Def1; :: thesis: verum

then dom (Shift (f,h)) = REAL by MEASURE6:24;

then A2: dom IT = dom (Shift (f,h)) by FUNCT_2:def 1;

assume A3: for x being Real holds IT . x = f . (x + h) ; :: thesis: IT = Shift (f,h)

for x being Element of REAL st x in dom IT holds

IT . x = (Shift (f,h)) . x

proof

hence
IT = Shift (f,h)
by A2, PARTFUN1:5; :: thesis: verum
let x be Element of REAL ; :: thesis: ( x in dom IT implies IT . x = (Shift (f,h)) . x )

assume x in dom IT ; :: thesis: IT . x = (Shift (f,h)) . x

then A4: x in (- h) ++ (dom f) by A2, Def1;

IT . x = f . (x + h) by A3;

hence IT . x = (Shift (f,h)) . x by A4, Def1; :: thesis: verum

end;assume x in dom IT ; :: thesis: IT . x = (Shift (f,h)) . x

then A4: x in (- h) ++ (dom f) by A2, Def1;

IT . x = f . (x + h) by A3;

hence IT . x = (Shift (f,h)) . x by A4, Def1; :: thesis: verum

( b