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) )_{1} being Function of V,W holds

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

( IT = Shift (f,h) iff for x being Element of V holds IT . x = f . (x + h) )

proof

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

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) ; :: thesis: IT = Shift (f,h)

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

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

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

( dom (Shift (f,h)) = (- h) ++ (dom f) & dom f = the carrier of V )
by Def1, FUNCT_2:def 1;assume A1:
IT = Shift (f,h)
; :: thesis: for x being Element of V holds IT . x = f . (x + h)

let x be Element of V; :: thesis: IT . x = f . (x + h)

dom (Shift (f,h)) = the carrier of V by A1, FUNCT_2:def 1;

then x in dom (Shift (f,h)) ;

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

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

end;let x be Element of V; :: thesis: IT . x = f . (x + h)

dom (Shift (f,h)) = the carrier of V by A1, FUNCT_2:def 1;

then x in dom (Shift (f,h)) ;

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

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

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) ; :: thesis: IT = Shift (f,h)

for x being Element of V 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 V; :: 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