:: deftheorem Def67 defines PathShift MODELC_1:def 67 :
for S being non empty set
for R being total Relation of S,S
for pai being inf_path of R
for k being Element of NAT
for b₅ being inf_path of R holds
( b₅ = PathShift (pai,k) iff for n being Element of NAT holds b₅ . n = pai . (n + k) );