for IT being Function of V,W holds
( IT = Shift (f,h) iff for x being Element of V holds IT . x = f . (x + h) )
proof
let IT be
Function of
V,
W;
( IT = Shift (f,h) iff for x being Element of V holds IT . x = f . (x + h) )
hereby ( ( for x being Element of V holds IT . x = f . (x + h) ) implies IT = Shift (f,h) )
end;
(
dom (Shift (f,h)) = (- h) ++ (dom f) &
dom f = the
carrier of
V )
by Def1, FUNCT_2:def 1;
then
dom (Shift (f,h)) = the
carrier of
V
by MEASURE624;
then A2:
dom IT = dom (Shift (f,h))
by FUNCT_2:def 1;
assume A3:
for
x being
Element of
V holds
IT . x = f . (x + h)
;
IT = Shift (f,h)
for
x being
Element of
V st
x in dom IT holds
IT . x = (Shift (f,h)) . x
hence
IT = Shift (
f,
h)
by A2, PARTFUN1:5;
verum
end;
hence
for b1 being Function of V,W holds
( b1 = Shift (f,h) iff for x being Element of V holds b1 . x = f . (x + h) )
; verum