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; :: thesis: ( IT = Shift (f,h) iff for x being Element of V holds IT . x = f . (x + h) )
hereby :: thesis: ( ( for x being Element of V holds IT . x = f . (x + h) ) implies IT = Shift (f,h) )
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 ;
then x in dom (Shift (f,h)) ;
then x in (- h) ++ (dom f) by Def1;
hence IT . x = f . (x + h) by ; :: thesis: verum
end;
( dom (Shift (f,h)) = (- h) ++ (dom f) & dom f = the carrier of V ) by ;
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
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 ;
IT . x = f . (x + h) by A3;
hence IT . x = (Shift (f,h)) . x by ; :: thesis: verum
end;
hence IT = Shift (f,h) by ; :: thesis: 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) ) ; :: thesis: verum