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

proof

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

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

assume A2: IT = Shift f,h ; :: thesis: for x being Real holds IT . x = f . (x + h)
then A3: dom (Shift f,h) = REAL by FUNCT_2:def 1;
let x be Real; :: thesis: IT . x = f . (x + h)
x in dom (Shift f,h) by A3;
then x in (- h) ++ (dom f) by Def1;
hence IT . x = f . (x + h) by A2, Def1; :: thesis: verum

end;

assume A4: for x being Real holds IT . x = f . (x + h) ; :: thesis: IT = Shift f,h
A5: dom (Shift f,h) = (- h) ++ (dom f) by Def1;
dom f = REAL by FUNCT_2:def 1;
then dom (Shift f,h) = REAL by A5, MEASURE6:60;
then A6: dom IT = dom (Shift f,h) by FUNCT_2:def 1;
for x being Element of REAL st x in dom IT holds
IT . x = (Shift f,h) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom IT implies IT . x = (Shift f,h) . x )
A7: IT . x = f . (x + h) by A4;
assume x in dom IT ; :: thesis: IT . x = (Shift f,h) . x
then x in (- h) ++ (dom f) by A6, Def1;
hence IT . x = (Shift f,h) . x by A7, Def1; :: thesis: verum

end;

hence IT = Shift f,h by A6, PARTFUN1:34; :: thesis: verum

end;

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